Theorem a2i 11

Description: Inference derived from axiom ax-2 6. (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 6	. 2 |- ((ph -> (ps -> ch)) -> ((ph -> ps) -> (ph -> ch)))
3	1, 2	ax-mp 7	1 |- ((ph -> ps) -> (ph -> ch))

Syntax hints:   -> wi 4

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

This theorem is referenced by:  imim2i  12  mpd  13  sylcom  25  pm2.43  47  ancl  301  ancr  304  anc2r  311  pm2.65  584  pm2.18dc  749  con4biddc  753  hbim1  1459  sbcof2  1688  ralimia  2376  ceqsalg  2576  rspct  2643  elabgt  2678  fvmptt  5205  bj-exlimmp  9244  bj-rspgt  9260  bj-indint  9390