Theorem a2i 14

Description: Inference distributing an antecedent. Inference associated with ax-2 7. Its associated inference is mpd 15. (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  15  imim2i  16  sylcom  30  pm2.43  56  ancl  544  ancr  546  anc2r  554  hbim1  2304  ralimia  3071  ceqsalgALT  3466  rspct  3550  fvmptt  6968  tfi  7804  fnfi  9112  imafiOLD  9226  finsschain  9269  ordiso2  9430  ordtypelem7  9439  dfom3  9568  infdiffi  9579  cantnfp1lem3  9601  cantnf  9614  r1ordg  9702  ttukeylem6  10436  fpwwe2lem7  10560  wunfi  10644  dfnn2  12187  trclfvcotr  14971  psgnunilem3  19471  pgpfac1  20057  fiuncmp  23369  filssufilg  23876  ufileu  23884  dfn0s2  28324  pjnormssi  32239  bnj1110  35124  waj-ax  36596  bj-nnclav  36806  bj-sb  36984  bj-equsal1  37131  bj-equsal2  37132  rdgeqoa  37686  wl-mps  37832  refimssco  44034  dfbi1ALTa  45366  simprimi  45367  natlocalincr  47306  atbiffatnnb  47360  rexrsb  47548  elsetrecslem  50174