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  2335  ralimia  3102  ceqsalgALT  3494  rspct  3570  fvmptt  7017  tfi  7858  fnfi  9172  finsschain  9326  ordiso2  9487  ordtypelem7  9496  dfom3  9626  infdiffi  9637  cantnfp1lem3  9659  cantnf  9672  r1ordg  9760  ttukeylem6  10516  fpwwe2lem7  10640  wunfi  10724  dfnn2  12264  trclfvcotr  15072  psgnunilem3  19597  pgpfac1  20183  fiuncmp  23598  filssufilg  24105  ufileu  24113  dfn0s2  28562  pjnormssi  32557  bnj1110  35402  waj-ax  36966  bj-nnclav  37175  bj-sb  37353  bj-equsal1  37500  bj-equsal2  37501  rdgeqoa  38057  wl-mps  38203  refimssco  44374  dfbi1ALTa  45689  simprimi  45690  natlocalincr  47633  atbiffatnnb  47690  rexrsb  47878  elsetrecslem  50518