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  546  ancr  548  anc2r  556  hbim1  2294  ralimia  3081  ceqsalgALT  3508  rspct  3598  elabgtOLD  3662  fvmptt  7014  tfi  7837  imafi  9171  fnfi  9177  finsschain  9355  ordiso2  9506  ordtypelem7  9515  dfom3  9638  infdiffi  9649  cantnfp1lem3  9671  cantnf  9684  r1ordg  9769  ttukeylem6  10505  fpwwe2lem7  10628  wunfi  10712  dfnn2  12221  trclfvcotr  14952  psgnunilem3  19357  pgpfac1  19942  fiuncmp  22890  filssufilg  23397  ufileu  23405  pjnormssi  31399  bnj1110  33931  waj-ax  35237  bj-nnclav  35360  bj-sb  35503  bj-equsal1  35640  bj-equsal2  35641  rdgeqoa  36189  wl-mps  36314  refimssco  42291  natlocalincr  45525  atbiffatnnb  45557  rexrsb  45743  elsetrecslem  47646