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  2332  ralimia  3099  ceqsalgALT  3491  rspct  3568  fvmptt  7012  tfi  7850  fnfi  9163  finsschain  9317  ordiso2  9478  ordtypelem7  9487  dfom3  9617  infdiffi  9628  cantnfp1lem3  9650  cantnf  9663  r1ordg  9751  ttukeylem6  10499  fpwwe2lem7  10623  wunfi  10707  dfnn2  12247  trclfvcotr  15048  psgnunilem3  19567  pgpfac1  20153  fiuncmp  23542  filssufilg  24049  ufileu  24057  dfn0s2  28506  pjnormssi  32501  bnj1110  35351  waj-ax  36906  bj-nnclav  37115  bj-sb  37293  bj-equsal1  37440  bj-equsal2  37441  rdgeqoa  37997  wl-mps  38143  refimssco  44316  dfbi1ALTa  45631  simprimi  45632  natlocalincr  47575  atbiffatnnb  47632  rexrsb  47820  elsetrecslem  50460