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

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-2 7

This theorem is referenced by:  mpd  16  imim2i  17  sylcom  31  pm2.43  57  ancl  553  ancr  555  anc2r  563  hbim1  2334  ralimia  3099  ceqsalgALT  3493  rspct  3570  fvmptt  7000  tfi  7837  fnfi  9150  finsschain  9304  ordiso2  9465  ordtypelem7  9474  dfom3  9604  infdiffi  9615  cantnfp1lem3  9637  cantnf  9650  r1ordg  9738  ttukeylem6  10486  fpwwe2lem7  10610  wunfi  10694  dfnn2  12234  trclfvcotr  15034  psgnunilem3  19554  pgpfac1  20140  fiuncmp  23518  filssufilg  24025  ufileu  24033  dfn0s2  28479  pjnormssi  32425  bnj1110  35282  waj-ax  36782  bj-nnclav  36991  bj-sb  37169  bj-equsal1  37316  bj-equsal2  37317  rdgeqoa  37871  wl-mps  38017  refimssco  44190  dfbi1ALTa  45507  simprimi  45508  natlocalincr  47451  atbiffatnnb  47505  rexrsb  47693  elsetrecslem  50329