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  3070  ceqsalgALT  3497  rspct  3587  fvmptt  7006  tfi  7848  fnfi  9192  imafiOLD  9326  finsschain  9371  ordiso2  9529  ordtypelem7  9538  dfom3  9661  infdiffi  9672  cantnfp1lem3  9694  cantnf  9707  r1ordg  9792  ttukeylem6  10528  fpwwe2lem7  10651  wunfi  10735  dfnn2  12253  trclfvcotr  15028  psgnunilem3  19477  pgpfac1  20063  fiuncmp  23342  filssufilg  23849  ufileu  23857  dfn0s2  28276  pjnormssi  32149  bnj1110  35013  waj-ax  36432  bj-nnclav  36564  bj-sb  36705  bj-equsal1  36842  bj-equsal2  36843  rdgeqoa  37388  wl-mps  37525  refimssco  43631  dfbi1ALTa  44964  simprimi  44965  natlocalincr  46905  atbiffatnnb  46941  rexrsb  47129  elsetrecslem  49563