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.18  122  ancl  568  ancr  571  anc2r  578  hbim1  2126  hbim1OLD  2231  ralimia  2950  ceqsalgALT  3222  rspct  3293  elabgt  3335  fvmptt  6257  tfi  7001  fnfi  8183  finsschain  8218  ordiso2  8365  ordtypelem7  8374  dfom3  8489  infdiffi  8500  cantnfp1lem3  8522  cantnf  8535  r1ordg  8586  ttukeylem6  9281  fpwwe2lem8  9404  wunfi  9488  dfnn2  10978  trclfvcotr  13679  psgnunilem3  17832  pgpfac1  18395  fiuncmp  21112  filssufilg  21620  ufileu  21628  pjnormssi  28867  bnj1110  30750  waj-ax  32028  bj-sb  32292  bj-equsal1  32427  bj-equsal2  32428  rdgeqoa  32823  wl-mps  32898  refimssco  37361  atbiffatnnb  40351  elsetrecslem  41692