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  2297  ralimia  3084  ceqsalgALT  3455  rspct  3537  elabgtOLD  3597  fvmptt  6877  tfi  7675  imafi  8920  fnfi  8925  finsschain  9056  ordiso2  9204  ordtypelem7  9213  dfom3  9335  infdiffi  9346  cantnfp1lem3  9368  cantnf  9381  r1ordg  9467  ttukeylem6  10201  fpwwe2lem7  10324  wunfi  10408  dfnn2  11916  trclfvcotr  14648  psgnunilem3  19019  pgpfac1  19598  fiuncmp  22463  filssufilg  22970  ufileu  22978  pjnormssi  30431  bnj1110  32862  waj-ax  34530  bj-nnclav  34653  bj-sb  34796  bj-equsal1  34934  bj-equsal2  34935  rdgeqoa  35468  wl-mps  35593  refimssco  41104  atbiffatnnb  44294  rexrsb  44479  elsetrecslem  46290