Theorem a2i 11

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 ) )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-2 7

This theorem is used by:  imim2i  12  mpd  13  sylcom  28  pm2.43  53  ancl  318  ancr  321  anc2r  328  pm2.65  669  pm2.18dc  867  con4biddc  869  hbim1  1623  sbcof2  1863  ralimia  2611  ceqsalg  2850  rspct  2922  elabgt  2967  fvmptt  5797  ordiso2  7375  bj-exlimmp  16797  bj-rspgt  16814  bj-indint  16957