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  552  ancr  554  anc2r  562  hbim1  2330  ralimia  3095  ceqsalgALT  3489  rspct  3566  fvmptt  6990  tfi  7827  fnfi  9139  imafiOLD  9253  finsschain  9295  ordiso2  9456  ordtypelem7  9465  dfom3  9595  infdiffi  9606  cantnfp1lem3  9628  cantnf  9641  r1ordg  9729  ttukeylem6  10464  fpwwe2lem7  10588  wunfi  10672  dfnn2  12216  trclfvcotr  15015  psgnunilem3  19526  pgpfac1  20112  fiuncmp  23451  filssufilg  23958  ufileu  23966  dfn0s2  28412  pjnormssi  32327  bnj1110  35237  waj-ax  36734  bj-nnclav  36944  bj-sb  37122  bj-equsal1  37269  bj-equsal2  37270  rdgeqoa  37824  wl-mps  37970  refimssco  44143  dfbi1ALTa  45475  simprimi  45476  natlocalincr  47412  atbiffatnnb  47466  rexrsb  47654  elsetrecslem  50280