CIC Proofs (3)

Th8) (P ⇒ Q), (Q ⇒ R), (R ⇒ S) ⊢ (P ⇒ S)

1.) ⊢ P ⇒ Q                        Hyp

2.) ⊢ Q ⇒ R                       Hyp

3.) ⊢ P ⇒ R                       Th5

4.) ⊢ R ⇒ S                        Hyp

5.) ⊢ P ⇒ S                         Th5 

Th9) H ⇒ (K ⇒ L), H ⇒ [K ⇒ (L ⇒ M)] ⊢ H ⇒ (K ⇒ M)

1.) ⊢ H ⇒ [K ⇒ (L ⇒ M)]                                                   Hyp

2.) ⊢ [K ⇒ ( L ⇒ M )] ⇒ [( K ⇒ L ) ⇒ ( K ⇒ M )]           Lk2

3.) ⊢ H ⇒ [( K ⇒ L ) ⇒ ( K ⇒ M )]                                   Th5

4.) ⊢ [H ⇒ ( K ⇒ L )] ⇒ [H ⇒ ( K ⇒ M )]                       Th2

5.) ⊢ H ⇒ (K ⇒ L)                                                               Hyp

6.) ⊢ H ⇒ ( K ⇒ M )                                                          MP 4,5

Th10) ⊢ [P ⇒ (P ⇒ Q)] ⇒ (P ⇒ Q)
1.) ⊢ P ⇒ P                                                               Th3
2.) ⊢ [P ⇒ (P ⇒ Q)] ⇒ P ⇒ P                                Th1
3.) ⊢ [P ⇒ (P ⇒ Q)] ⇒ [(P ⇒ P) ⇒ (P ⇒ Q)]       Lk2
4.) ⊢ [P ⇒ (P ⇒ Q)] ⇒ (P ⇒ Q)                            Th4