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  pm2.18OLD  129  ancl  547  ancr  549  anc2r  557  hbim1  2301  ralimia  3158  ceqsalgALT  3530  rspct  3608  elabgt  3662  fvmptt  6782  tfi  7562  fnfi  8790  finsschain  8825  ordiso2  8973  ordtypelem7  8982  dfom3  9104  infdiffi  9115  cantnfp1lem3  9137  cantnf  9150  r1ordg  9201  ttukeylem6  9930  fpwwe2lem8  10053  wunfi  10137  dfnn2  11645  trclfvcotr  14363  psgnunilem3  18618  pgpfac1  19196  fiuncmp  22006  filssufilg  22513  ufileu  22521  pjnormssi  29939  bnj1110  32249  waj-ax  33757  bj-nnclav  33879  bj-peircestab  33883  bj-sb  34016  bj-equsal1  34142  bj-equsal2  34143  rdgeqoa  34645  wl-mps  34741  refimssco  39960  atbiffatnnb  43142  elsetrecslem  44795