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  3063  ceqsalgALT  3475  rspct  3565  fvmptt  6954  tfi  7793  fnfi  9102  imafiOLD  9223  finsschain  9268  ordiso2  9426  ordtypelem7  9435  dfom3  9562  infdiffi  9573  cantnfp1lem3  9595  cantnf  9608  r1ordg  9693  ttukeylem6  10427  fpwwe2lem7  10550  wunfi  10634  dfnn2  12159  trclfvcotr  14934  psgnunilem3  19393  pgpfac1  19979  fiuncmp  23307  filssufilg  23814  ufileu  23822  dfn0s2  28247  pjnormssi  32130  bnj1110  34951  waj-ax  36390  bj-nnclav  36522  bj-sb  36663  bj-equsal1  36800  bj-equsal2  36801  rdgeqoa  37346  wl-mps  37483  refimssco  43583  dfbi1ALTa  44916  simprimi  44917  natlocalincr  46861  atbiffatnnb  46900  rexrsb  47088  elsetrecslem  49688