CIC Proofs (1)

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

Th5) H ⇒ K, K ⇒ L ⊢ H ⇒ L

1.) ⊢ H ⇒ K                                       Hyp

2.) ⊢ K ⇒ L                                       Hyp

3.) ⊢ H ⇒ (K ⇒ L)                                Th1

4.) ⊢ (H ⇒ K) ⇒ (H ⇒ L)               Th2

5.) ⊢ H ⇒ L                                      MP 1,4