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  2297  ralimia  3064  ceqsalgALT  3487  rspct  3577  fvmptt  6991  tfi  7832  fnfi  9148  imafiOLD  9272  finsschain  9317  ordiso2  9475  ordtypelem7  9484  dfom3  9607  infdiffi  9618  cantnfp1lem3  9640  cantnf  9653  r1ordg  9738  ttukeylem6  10474  fpwwe2lem7  10597  wunfi  10681  dfnn2  12206  trclfvcotr  14982  psgnunilem3  19433  pgpfac1  20019  fiuncmp  23298  filssufilg  23805  ufileu  23813  dfn0s2  28231  pjnormssi  32104  bnj1110  34979  waj-ax  36409  bj-nnclav  36541  bj-sb  36682  bj-equsal1  36819  bj-equsal2  36820  rdgeqoa  37365  wl-mps  37502  refimssco  43603  dfbi1ALTa  44936  simprimi  44937  natlocalincr  46881  atbiffatnnb  46917  rexrsb  47105  elsetrecslem  49692