Propositional Calculus Proofs (9)

Th31) ⊢ (H ⇒ K) ⇒ {(H ⇒ L) ⇒ [H ⇒ (K ∧ L)]}

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

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

3.) ⊢ {H ⇒ [K ⇒ (L ⇒ (K ∧ L))]} ⇒ {(H ⇒ K) ⇒ [(H ⇒ L) ⇒ (H ⇒ (K ∧ L))]}       Th14

4.) ⊢ K ⇒ (L ⇒ (K ∧ L))                                                                                               Th30

5.) ⊢ H ⇒ {K ⇒ [L ⇒ (K ∧ L)]}                                                                                   Th1

6.) ⊢ (H ⇒ K) ⇒ {(H ⇒ L) ⇒ [H ⇒ (K ∧ L)]}                                                             MP 3,5

Th32) ⊢ [H ⇒ (K ∧ L)] ⇒ (H ⇒ L)

1.) ⊢ (K ∧ L) ⇒ L                                                                          Th28

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

3.) ⊢ {H ⇒ [(K ∧ L) ⇒ L]} ⇒ {[H ⇒ (K ∧ L)] ⇒ (H ⇒ L)}        Lk2

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

Th33) ⊢ [H ⇒ (K ∧ L)] ⇒ (H ⇒ K)

1.) ⊢ (K ∧ L) ⇒ K                                                                          Th29

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

3.) ⊢ {H ⇒ [(K ∧ L) ⇒ K]} ⇒ {[H ⇒ (K ∧ L)] ⇒ (H ⇒ K)}        Lk2

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

Th34) ⊢ P ⇒ (P ∧ P)     Idempotency of ∧

1.) ⊢ (P ⇒ P) ⇒ {(P ⇒ P) ⇒ [P ⇒ (P ∧ P)]}                                  Th31

2.) ⊢ P ⇒ P                                                                                     Th3

3.) ⊢ (P ⇒ P) ⇒ [P ⇒ (P ∧ P)]                                                       MP 1,2

4.) ⊢ P ⇒ (P ∧ P)                                                                            MP 2,3