Theorem a2i 14

Description: Inference distributing an antecedent. Inference associated with ax-2 7. Its associated inference is mpd 15. (Contributed by NM, 29-Dec-1992.)

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:  mpd  15  imim2i  16  sylcom  30  pm2.43  56  pm2.18  122  ancl  569  ancr  572  anc2r  579  hbim1  2125  hbim1OLD  2227  ralimia  2950  ceqsalgALT  3231  rspct  3302  elabgt  3347  fvmptt  6300  tfi  7053  fnfi  8238  finsschain  8273  ordiso2  8420  ordtypelem7  8429  dfom3  8544  infdiffi  8555  cantnfp1lem3  8577  cantnf  8590  r1ordg  8641  ttukeylem6  9336  fpwwe2lem8  9459  wunfi  9543  dfnn2  11033  trclfvcotr  13750  psgnunilem3  17916  pgpfac1  18479  fiuncmp  21207  filssufilg  21715  ufileu  21723  pjnormssi  29027  bnj1110  31050  waj-ax  32413  bj-sb  32677  bj-equsal1  32811  bj-equsal2  32812  rdgeqoa  33218  wl-mps  33290  refimssco  37913  atbiffatnnb  41079  elsetrecslem  42444