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  3558  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  19408  pgpfac1  19994  fiuncmp  23319  filssufilg  23826  ufileu  23834  dfn0s2  28260  pjnormssi  32148  bnj1110  34994  waj-ax  36458  bj-nnclav  36590  bj-sb  36731  bj-equsal1  36868  bj-equsal2  36869  rdgeqoa  37414  wl-mps  37551  refimssco  43699  dfbi1ALTa  45031  simprimi  45032  natlocalincr  46973  atbiffatnnb  47011  rexrsb  47199  elsetrecslem  49799