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  3072  ceqsalgALT  3479  rspct  3564  fvmptt  6970  tfi  7805  fnfi  9114  imafiOLD  9228  finsschain  9271  ordiso2  9432  ordtypelem7  9441  dfom3  9568  infdiffi  9579  cantnfp1lem3  9601  cantnf  9614  r1ordg  9702  ttukeylem6  10436  fpwwe2lem7  10560  wunfi  10644  dfnn2  12170  trclfvcotr  14944  psgnunilem3  19437  pgpfac1  20023  fiuncmp  23360  filssufilg  23867  ufileu  23875  dfn0s2  28340  pjnormssi  32255  bnj1110  35157  waj-ax  36627  bj-nnclav  36765  bj-sb  36929  bj-equsal1  37069  bj-equsal2  37070  rdgeqoa  37622  wl-mps  37759  refimssco  43960  dfbi1ALTa  45292  simprimi  45293  natlocalincr  47231  atbiffatnnb  47269  rexrsb  47457  elsetrecslem  50055