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  2305  ralimia  3160  ceqsalgALT  3532  rspct  3611  elabgt  3665  fvmptt  6790  tfi  7570  fnfi  8798  finsschain  8833  ordiso2  8981  ordtypelem7  8990  dfom3  9112  infdiffi  9123  cantnfp1lem3  9145  cantnf  9158  r1ordg  9209  ttukeylem6  9938  fpwwe2lem8  10061  wunfi  10145  dfnn2  11653  trclfvcotr  14371  psgnunilem3  18626  pgpfac1  19204  fiuncmp  22014  filssufilg  22521  ufileu  22529  pjnormssi  29947  bnj1110  32256  waj-ax  33764  bj-nnclav  33886  bj-peircestab  33890  bj-sb  34023  bj-equsal1  34149  bj-equsal2  34150  rdgeqoa  34653  wl-mps  34749  refimssco  39974  atbiffatnnb  43155  rexrsb  43305  elsetrecslem  44808