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  2301  ralimia  3067  ceqsalgALT  3474  rspct  3559  fvmptt  6957  tfi  7791  fnfi  9096  imafiOLD  9209  finsschain  9252  ordiso2  9410  ordtypelem7  9419  dfom3  9546  infdiffi  9557  cantnfp1lem3  9579  cantnf  9592  r1ordg  9680  ttukeylem6  10414  fpwwe2lem7  10537  wunfi  10621  dfnn2  12147  trclfvcotr  14920  psgnunilem3  19412  pgpfac1  19998  fiuncmp  23322  filssufilg  23829  ufileu  23837  dfn0s2  28263  pjnormssi  32152  bnj1110  35017  waj-ax  36481  bj-nnclav  36613  bj-sb  36754  bj-equsal1  36891  bj-equsal2  36892  rdgeqoa  37437  wl-mps  37574  refimssco  43727  dfbi1ALTa  45059  simprimi  45060  natlocalincr  47001  atbiffatnnb  47039  rexrsb  47227  elsetrecslem  49827