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  549  ancr  551  anc2r  559  hbim1  2308  ralimia  3074  ceqsalgALT  3469  rspct  3553  fvmptt  6963  tfi  7800  fnfi  9109  imafiOLD  9223  finsschain  9266  ordiso2  9427  ordtypelem7  9436  dfom3  9566  infdiffi  9577  cantnfp1lem3  9599  cantnf  9612  r1ordg  9700  ttukeylem6  10434  fpwwe2lem7  10558  wunfi  10642  dfnn2  12185  trclfvcotr  14969  psgnunilem3  19469  pgpfac1  20055  fiuncmp  23394  filssufilg  23901  ufileu  23909  dfn0s2  28349  pjnormssi  32264  bnj1110  35171  waj-ax  36649  bj-nnclav  36859  bj-sb  37037  bj-equsal1  37184  bj-equsal2  37185  rdgeqoa  37739  wl-mps  37885  refimssco  44058  dfbi1ALTa  45390  simprimi  45391  natlocalincr  47328  atbiffatnnb  47382  rexrsb  47570  elsetrecslem  50196