Мат логика, помогите сделать дедуктивный вывод

[Knopick]

Помогите сделать дедуктивный вывод (ввод посылки, удаление импликации, удаление конъюнкции и т.п.). надо ОЧЕНЬ, пожалуйста
1) {A <-> B} |- (C v A) <-> (C v B)
2) {A & B v -A & -B} |- (A -> C) <-> (B -> C)

-A и -B = отрицание A и отрицание B