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  545  ancr  547  anc2r  555  hbim1  2294  ralimia  3085  ceqsalgALT  3465  rspct  3547  elabgtOLD  3604  fvmptt  6895  tfi  7700  imafi  8958  fnfi  8964  finsschain  9126  ordiso2  9274  ordtypelem7  9283  dfom3  9405  infdiffi  9416  cantnfp1lem3  9438  cantnf  9451  r1ordg  9536  ttukeylem6  10270  fpwwe2lem7  10393  wunfi  10477  dfnn2  11986  trclfvcotr  14720  psgnunilem3  19104  pgpfac1  19683  fiuncmp  22555  filssufilg  23062  ufileu  23070  pjnormssi  30530  bnj1110  32962  waj-ax  34603  bj-nnclav  34726  bj-sb  34869  bj-equsal1  35007  bj-equsal2  35008  rdgeqoa  35541  wl-mps  35666  refimssco  41215  atbiffatnnb  44407  rexrsb  44592  elsetrecslem  46404  natlocalincr  46511