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  543  ancr  545  anc2r  553  hbim1  2287  ralimia  3070  ceqsalgALT  3499  rspct  3594  elabgtOLDOLD  3661  fvmptt  7031  tfi  7865  fnfi  9217  imafiOLD  9358  finsschain  9405  ordiso2  9560  ordtypelem7  9569  dfom3  9692  infdiffi  9703  cantnfp1lem3  9725  cantnf  9738  r1ordg  9823  ttukeylem6  10559  fpwwe2lem7  10682  wunfi  10766  dfnn2  12279  trclfvcotr  15016  psgnunilem3  19496  pgpfac1  20082  fiuncmp  23402  filssufilg  23909  ufileu  23917  dfn0s2  28307  pjnormssi  32104  bnj1110  34829  waj-ax  36128  bj-nnclav  36251  bj-sb  36394  bj-equsal1  36531  bj-equsal2  36532  rdgeqoa  37079  wl-mps  37204  refimssco  43292  natlocalincr  46513  atbiffatnnb  46545  rexrsb  46731  elsetrecslem  48463