Propositional Calculus Proofs (13)

Th52.) ⊢ [H ⇒ (K ∧ L)] ⇒ [(H ⇒ L) ∧ (H ⇒ K)]
1.) ⊢ {[H ⇒ (K ∧ L)] ⇒ (H ⇒ L)} ⇒ {([H ⇒ (K ∧ L)] ⇒ (H ⇒ K)) ⇒ [[H ⇒ (K ∧ L)] ⇒ ((H ⇒ L) ∧ (H ⇒ K))]}                                                                                                               Th37

2.) ⊢ [H ⇒ (K ∧ L)] ⇒ (H ⇒ L)                                                                                      Th38

3.) ⊢ [H ⇒ (K ∧ L)] ⇒ (H ⇒ K)                                                                                      Th39

4.) ⊢ {([H ⇒ (K ∧ L)] ⇒ (H ⇒ K)) ⇒ [[H ⇒ (K ∧ L)] ⇒ ((H ⇒ L) ∧ (H ⇒ K))]}       MP 1,2

5.) ⊢ [H ⇒ (K ∧ L)] ⇒ [(H ⇒ L) ∧ (H ⇒ K)]                                                                 MP 3,4

Th53.) (A ⇔ B) ⊢ (¬A ⇔ ¬B)
1.) ⊢ A ⇔ B                                                                                                Hyp
2.) ⊢ (A ⇒ B) ∧ (B ⇒ A)                                                                            Definition of ⇔
3.) ⊢ [(A ⇒ B) ∧ (B ⇒ A)] ⇒ (A ⇒ B)                                                       Th35
4.) ⊢ [(A ⇒ B) ∧ (B ⇒ A)] ⇒ (B ⇒ A)                                                       Th34
5.) ⊢ (A ⇒ B)                                                                                              MP 2,3
6.) ⊢ (B ⇒ A)                                                                                              MP 2,4
7.) ⊢ (A ⇒ B) ⇒ (¬B ⇒ ¬A)                                                                       Th29
8.) ⊢ (B ⇒ A) ⇒ (¬A ⇒ ¬B)                                                                       Th29
9.) ⊢ ¬B ⇒ ¬A                                                                                            MP 5,7
10.) ⊢ ¬A ⇒ ¬B                                                                                           MP 6,8
11.) ⊢ (¬B ⇒ ¬A) ⇒ [(¬A ⇒ ¬B) ⇒ ((¬B ⇒ ¬A) ∧ (¬A ⇒ ¬B))]             Th36
12.) ⊢ (¬A ⇒ ¬B) ⇒ ((¬B ⇒ ¬A) ∧ (¬A ⇒ ¬B))                                       MP 9,11
13.) ⊢ [(¬B ⇒ ¬A) ∧ (¬A ⇒ ¬B)]                                                              MP 10,12
14.) ⊢ ¬B ⇔ ¬A                                                                                          Definition of ⇔
15.) ⊢ ¬A ⇔ ¬B                                                                                          Th41 

Th54.) ⊢ P ⇔ P
1.) ⊢ P ⇒ P                                Th3
2.) ⊢ P ⇒ P                               Th3
3.) ⊢ P ⇔ P                               Th40