Theorem a2i 15

Description: Inference distributing an antecedent. Inference associated with ax-2 7. Its associated inference is mpd 16. (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 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-2 7

This theorem is used by:  mpd  16  imim2i  17  sylcom  31  pm2.43  57  ancl  554  ancr  556  anc2r  564  hbim1  2334  ralimia  3100  ceqsalgALT  3490  rspct  3566  fvmptt  7040  tfi  7891  fnfi  9224  finsschain  9379  ordiso2  9539  ordtypelem7  9548  dfom3  9678  infdiffi  9689  cantnfp1lem3  9711  cantnf  9724  r1ordg  9815  ttukeylem6  10622  fpwwe2lem7  10752  wunfi  10836  dfnn2  12378  trclfvcotr  15194  psgnunilem3  19743  pgpfac1  20329  fiuncmp  23755  filssufilg  24263  ufileu  24271  dfn0s2  28751  pjnormssi  32803  bnj1110  35695  waj-ax  37393  bj-nnclav  37602  bj-sb  37780  bj-equsal1  37927  bj-equsal2  37928  rdgeqoa  38498  wl-mps  38644  refimssco  44810  dfbi1ALTa  46135  simprimi  46136  atbiffatnnb  48197  rexrsb  48386  elsetrecslem  51082