hypothetical_syllogism

Theorem hypothetical_syllogism

Theorem. hypothetical_syllogism
(A → B) → (B → C) → (A → C)

Proof
01. 1 ⊢ A → B, hypo.
02. 2 ⊢ B → C, hypo.
03. 3 ⊢ A, hypo.
04. 1, 3 ⊢ B, subj_elim 1 3.
05. 1, 2, 3 ⊢ C, subj_elim 2 4.
hypothetical_syllogism. ⊢ (A → B) → (B → C) → (A → C),
  subj_intro_iii 5.