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  2331  ralimia  3097  ceqsalgALT  3487  rspct  3563  fvmptt  7006  tfi  7853  fnfi  9177  finsschain  9332  ordiso2  9493  ordtypelem7  9502  dfom3  9632  infdiffi  9643  cantnfp1lem3  9665  cantnf  9678  r1ordg  9768  ttukeylem6  10573  fpwwe2lem7  10703  wunfi  10787  dfnn2  12329  trclfvcotr  15142  psgnunilem3  19690  pgpfac1  20276  fiuncmp  23702  filssufilg  24210  ufileu  24218  dfn0s2  28700  pjnormssi  32752  bnj1110  35595  waj-ax  37172  bj-nnclav  37381  bj-sb  37559  bj-equsal1  37706  bj-equsal2  37707  rdgeqoa  38261  wl-mps  38407  refimssco  44566  dfbi1ALTa  45881  simprimi  45882  atbiffatnnb  47926  rexrsb  48114  elsetrecslem  50736