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  ancl  544  ancr  546  anc2r  554  hbim1  2297  ralimia  3080  ceqsalgALT  3518  rspct  3608  fvmptt  7036  tfi  7874  fnfi  9218  imafiOLD  9354  finsschain  9399  ordiso2  9555  ordtypelem7  9564  dfom3  9687  infdiffi  9698  cantnfp1lem3  9720  cantnf  9733  r1ordg  9818  ttukeylem6  10554  fpwwe2lem7  10677  wunfi  10761  dfnn2  12279  trclfvcotr  15048  psgnunilem3  19514  pgpfac1  20100  fiuncmp  23412  filssufilg  23919  ufileu  23927  dfn0s2  28336  pjnormssi  32187  bnj1110  34996  waj-ax  36415  bj-nnclav  36547  bj-sb  36688  bj-equsal1  36825  bj-equsal2  36826  rdgeqoa  37371  wl-mps  37508  refimssco  43620  dfbi1ALTa  44960  simprimi  44961  natlocalincr  46891  atbiffatnnb  46924  rexrsb  47112  elsetrecslem  49218