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  2295  ralimia  3077  ceqsalgALT  3515  rspct  3607  elabgtOLDOLD  3673  fvmptt  7035  tfi  7873  fnfi  9215  imafiOLD  9351  finsschain  9396  ordiso2  9552  ordtypelem7  9561  dfom3  9684  infdiffi  9695  cantnfp1lem3  9717  cantnf  9730  r1ordg  9815  ttukeylem6  10551  fpwwe2lem7  10674  wunfi  10758  dfnn2  12276  trclfvcotr  15044  psgnunilem3  19528  pgpfac1  20114  fiuncmp  23427  filssufilg  23934  ufileu  23942  dfn0s2  28350  pjnormssi  32196  bnj1110  34974  waj-ax  36396  bj-nnclav  36528  bj-sb  36669  bj-equsal1  36806  bj-equsal2  36807  rdgeqoa  37352  wl-mps  37487  refimssco  43596  natlocalincr  46829  atbiffatnnb  46861  rexrsb  47049  elsetrecslem  48929