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  2332  ralimia  3098  ceqsalgALT  3489  rspct  3565  fvmptt  7011  tfi  7853  fnfi  9176  finsschain  9330  ordiso2  9491  ordtypelem7  9500  dfom3  9630  infdiffi  9641  cantnfp1lem3  9663  cantnf  9676  r1ordg  9764  ttukeylem6  10520  fpwwe2lem7  10650  wunfi  10734  dfnn2  12274  trclfvcotr  15086  psgnunilem3  19629  pgpfac1  20215  fiuncmp  23635  filssufilg  24143  ufileu  24151  dfn0s2  28605  pjnormssi  32657  bnj1110  35499  waj-ax  37041  bj-nnclav  37250  bj-sb  37428  bj-equsal1  37575  bj-equsal2  37576  rdgeqoa  38132  wl-mps  38278  refimssco  44455  dfbi1ALTa  45770  simprimi  45771  atbiffatnnb  47808  rexrsb  47996  elsetrecslem  50633