Theorem a2i 8

Description: Inference derived from axiom ax-2 4.

Hypothesis

Ref	Expression
a2i.1	⊢ (φ → (ψ → χ))

Assertion

Ref	Expression
a2i	⊢ ((φ → ψ) → (φ → χ))

Proof of Theorem a2i

Step	Hyp	Ref	Expression
1		a2i.1	. 2 ⊢ (φ → (ψ → χ))
2		ax-2 4	. 2 ⊢ ((φ → (ψ → χ)) → ((φ → ψ) → (φ → χ)))
3	1, 2	ax-mp 6	1 ⊢ ((φ → ψ) → (φ → χ))

Syntax hints:   → wi 2

This theorem is referenced by:  id 9  syl 12  com12 13  syl3 18  syld 27  mpd 46  pm2.43 57  pm2.18 75  pm2.65 115  ancl 242  ancr 243  anc2l 248  anc2r 249  hbim1 781  r19.20i 1253  ceqsalg 1362  tfi 2244  dfom3 3477  peano2nn 4433  pjnormss 5638

This theorem was proved from axioms:  ax-2 4  ax-mp 6

metamath.org