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

Syntax hints:   -> wi 4

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

This theorem is referenced by:  imim2i  12  mpd  13  sylcom  28  pm2.43  53  ancl  316  ancr  319  anc2r  326  pm2.65  654  pm2.18dc  850  con4biddc  852  hbim1  1563  sbcof2  1803  ralimia  2531  ceqsalg  2758  rspct  2827  elabgt  2871  fvmptt  5587  ordiso2  7012  bj-exlimmp  13804  bj-rspgt  13821  bj-indint  13966