Theorem a2i 12

Description: Inference derived from Axiom ax-2 7. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
a2i.1	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
a2i	|- ((ph -> ps) -> (ph -> ch))

Proof of Theorem a2i

Step	Hyp	Ref	Expression
1		a2i.1	. 2 |- (ph -> (ps -> ch))
2		ax-2 7	. 2 |- ((ph -> (ps -> ch)) -> ((ph -> ps) -> (ph -> ch)))
3	1, 2	ax-mp 5	1 |- ((ph -> ps) -> (ph -> ch))

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-2 7

This theorem is referenced by:  imim2i  13  mpd  14  sylcom  25  pm2.43  47  pm2.18  102  ancl  529  ancr  532  anc2r  539  hbim1  1810  nfim1OLD  1812  dvelimv  1939  ralimia  2688  ceqsalg  2884  rspct  2949  elabgt  2983  peano2  4404  peano5  4410  spfininduct  4541  fvopab4t  5386