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  2301  ralimia  3086  ceqsalgALT  3526  rspct  3621  elabgtOLDOLD  3687  fvmptt  7049  tfi  7890  fnfi  9244  imafiOLD  9382  finsschain  9429  ordiso2  9584  ordtypelem7  9593  dfom3  9716  infdiffi  9727  cantnfp1lem3  9749  cantnf  9762  r1ordg  9847  ttukeylem6  10583  fpwwe2lem7  10706  wunfi  10790  dfnn2  12306  trclfvcotr  15058  psgnunilem3  19538  pgpfac1  20124  fiuncmp  23433  filssufilg  23940  ufileu  23948  dfn0s2  28354  pjnormssi  32200  bnj1110  34958  waj-ax  36380  bj-nnclav  36512  bj-sb  36653  bj-equsal1  36790  bj-equsal2  36791  rdgeqoa  37336  wl-mps  37461  refimssco  43569  natlocalincr  46795  atbiffatnnb  46827  rexrsb  47015  elsetrecslem  48791