CIC Proofs (5)

Th12) ⊢ (P ⇒ Q) ⇒ [(Q ⇒ R) ⇒ (P ⇒ R)]
1.) (P ⇒ Q) ⇒ [(Q ⇒ R) ⇒ (P ⇒ Q)]                                    Lk1
2.) ⊢ (Q ⇒ R) ⇒ [(P ⇒ Q) ⇒ (P ⇒ R)]                                Th11
3.) ⊢ (P ⇒ Q) ⇒ {(Q ⇒ R) ⇒ [(P ⇒ Q) ⇒ (P ⇒ R)]}         Th1
4.) ⊢ (P ⇒ Q) ⇒ [(Q ⇒ R) ⇒ (P ⇒ R)]                                 Th9

Th13) A ⇒ (B ⇒ C), (D ⇒ B) ⊢ A ⇒ (D ⇒ C)

1.) ⊢ D ⇒ B                                                            Hyp
2.) ⊢ (D ⇒ B) ⇒ [(B ⇒ C) ⇒ (D ⇒ C)]              Th12

3.) ⊢ (B ⇒ C) ⇒ (D ⇒ C)                                     MP 1,2

4.) ⊢ A ⇒ (B ⇒ C)                                                Hyp

5.) ⊢ A ⇒ (D ⇒ C)                                                Th5

Th14) O ⇒ (U ⇒ V), (V ⇒ W) ⊢ O ⇒ (U ⇒ W)
 1.) ⊢ V ⇒ W                                                          Hyp
2.) ⊢ (V ⇒ W) ⇒ [(U ⇒ V) ⇒ (U ⇒ W)]           Th11
3.) ⊢ (U ⇒ V) ⇒ (U ⇒ W)                                   MP 1,2
4.) ⊢ O ⇒ (U ⇒ V)                                                Hyp
5.) ⊢ O ⇒ (U ⇒ W)                                               Th5

Th15) ⊢ [G ⇒ (H ⇒ J)] ⇒ [H ⇒ (G ⇒ J)]       Law of Commutation
1.) ⊢ [G ⇒ (H ⇒ J)] ⇒ [(G ⇒ H) ⇒ (G ⇒ J)]    Lk2
2.) ⊢ H ⇒ (G ⇒ H)                                              Lk1
3.) ⊢ [G ⇒ (H ⇒ J)] ⇒ [H ⇒ (G ⇒ J)]               Th13

Th16) ⊢ A ⇒ [(A ⇒ B) ⇒ B]                                Law of Assertion
1.) ⊢ (A ⇒ B) ⇒ (A ⇒ B)                                        Th3
2.) ⊢ [(A ⇒ B) ⇒ A] ⇒ [(A ⇒ B) ⇒ B]                 Th2
3.) ⊢ A ⇒ [(A ⇒ B) ⇒ A ]                                       Lk1
4.) ⊢ A ⇒  [(A ⇒ B) ⇒ B]                                       Th5