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  2303  ralimia  3070  ceqsalgALT  3477  rspct  3562  fvmptt  6961  tfi  7795  fnfi  9102  imafiOLD  9216  finsschain  9259  ordiso2  9420  ordtypelem7  9429  dfom3  9556  infdiffi  9567  cantnfp1lem3  9589  cantnf  9602  r1ordg  9690  ttukeylem6  10424  fpwwe2lem7  10548  wunfi  10632  dfnn2  12158  trclfvcotr  14932  psgnunilem3  19425  pgpfac1  20011  fiuncmp  23348  filssufilg  23855  ufileu  23863  dfn0s2  28328  pjnormssi  32243  bnj1110  35138  waj-ax  36608  bj-nnclav  36746  bj-sb  36888  bj-equsal1  37025  bj-equsal2  37026  rdgeqoa  37575  wl-mps  37712  refimssco  43848  dfbi1ALTa  45180  simprimi  45181  natlocalincr  47120  atbiffatnnb  47158  rexrsb  47346  elsetrecslem  49944