CIC Proofs (2)

Th6) K, H ⇒ ( K ⇒ L ) ⊢ H ⇒ L
1.) ⊢ [H ⇒ ( K ⇒ L )] ⇒ [( H ⇒ K ) ⇒ ( H ⇒ L )]      Lk2
2.) ⊢ H ⇒ ( K ⇒ L )                                                        Hyp
3.) ⊢ ( H ⇒ K ) ⇒ ( H ⇒ L )                                          MP 1,2
4.) ⊢ K                                                                              Hyp
5.) ⊢ H ⇒ K                                                                     Th1
6.) ⊢ H ⇒ L                                                                     MP 3,5

Th7) P ⇒ Q, P ⇒ ( Q ⇒ R ), P ⇒ ( R ⇒ S ) ⊢ P ⇒ S
1.) ⊢ P ⇒ Q                                         Hyp
2.) ⊢ P ⇒ ( Q ⇒ R )                           Hyp
3.) ⊢ P ⇒ R                                         Th4
4.) ⊢ P ⇒ ( R ⇒ S )                            Hyp
5.) ⊢ P ⇒ S                                          Th4