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  pm2.18  125  ancl  540  ancr  542  anc2r  550  hbim1  2272  ralimia  3132  ceqsalgALT  3433  rspct  3504  elabgt  3553  fvmptt  6563  tfi  7333  fnfi  8528  finsschain  8563  ordiso2  8711  ordtypelem7  8720  dfom3  8843  infdiffi  8854  cantnfp1lem3  8876  cantnf  8889  r1ordg  8940  ttukeylem6  9673  fpwwe2lem8  9796  wunfi  9880  dfnn2  11393  trclfvcotr  14161  psgnunilem3  18304  pgpfac1  18870  fiuncmp  21620  filssufilg  22127  ufileu  22135  pjnormssi  29603  bnj1110  31653  waj-ax  33000  bj-sb  33270  bj-equsal1  33390  bj-equsal2  33391  rdgeqoa  33816  wl-mps  33888  refimssco  38880  atbiffatnnb  42016  elsetrecslem  43560