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  545  ancr  547  anc2r  555  hbim1  2298  ralimia  3087  ceqsalgALT  3464  rspct  3546  elabgtOLD  3606  fvmptt  6890  tfi  7692  imafi  8938  fnfi  8944  finsschain  9102  ordiso2  9250  ordtypelem7  9259  dfom3  9381  infdiffi  9392  cantnfp1lem3  9414  cantnf  9427  r1ordg  9535  ttukeylem6  10269  fpwwe2lem7  10392  wunfi  10476  dfnn2  11984  trclfvcotr  14716  psgnunilem3  19100  pgpfac1  19679  fiuncmp  22551  filssufilg  23058  ufileu  23066  pjnormssi  30524  bnj1110  32956  waj-ax  34597  bj-nnclav  34720  bj-sb  34863  bj-equsal1  35001  bj-equsal2  35002  rdgeqoa  35535  wl-mps  35660  refimssco  41183  atbiffatnnb  44373  rexrsb  44558  elsetrecslem  46371