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	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
a2i	⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒))

Proof of Theorem a2i

Step	Hyp	Ref	Expression
1		a2i.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		ax-2 7	. 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
3	1, 2	ax-mp 5	1 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒))

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.18OLD  129  ancl  548  ancr  550  anc2r  558  hbim1  2301  ralimia  3126  ceqsalgALT  3477  rspct  3557  elabgt  3609  fvmptt  6765  tfi  7548  fnfi  8780  finsschain  8815  ordiso2  8963  ordtypelem7  8972  dfom3  9094  infdiffi  9105  cantnfp1lem3  9127  cantnf  9140  r1ordg  9191  ttukeylem6  9925  fpwwe2lem8  10048  wunfi  10132  dfnn2  11638  trclfvcotr  14360  psgnunilem3  18616  pgpfac1  19195  fiuncmp  22009  filssufilg  22516  ufileu  22524  pjnormssi  29951  bnj1110  32364  waj-ax  33875  bj-nnclav  33997  bj-peircestab  34001  bj-sb  34134  bj-equsal1  34262  bj-equsal2  34263  rdgeqoa  34787  wl-mps  34912  refimssco  40307  atbiffatnnb  43505  rexrsb  43655  elsetrecslem  45228