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  2299  ralimia  3066  ceqsalgALT  3473  rspct  3563  fvmptt  6949  tfi  7783  fnfi  9087  imafiOLD  9200  finsschain  9243  ordiso2  9401  ordtypelem7  9410  dfom3  9537  infdiffi  9548  cantnfp1lem3  9570  cantnf  9583  r1ordg  9671  ttukeylem6  10405  fpwwe2lem7  10528  wunfi  10612  dfnn2  12138  trclfvcotr  14916  psgnunilem3  19409  pgpfac1  19995  fiuncmp  23320  filssufilg  23827  ufileu  23835  dfn0s2  28261  pjnormssi  32146  bnj1110  34992  waj-ax  36454  bj-nnclav  36586  bj-sb  36727  bj-equsal1  36864  bj-equsal2  36865  rdgeqoa  37410  wl-mps  37547  refimssco  43646  dfbi1ALTa  44978  simprimi  44979  natlocalincr  46920  atbiffatnnb  46949  rexrsb  47137  elsetrecslem  49737