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  3063  ceqsalgALT  3484  rspct  3574  fvmptt  6988  tfi  7829  fnfi  9142  imafiOLD  9265  finsschain  9310  ordiso2  9468  ordtypelem7  9477  dfom3  9600  infdiffi  9611  cantnfp1lem3  9633  cantnf  9646  r1ordg  9731  ttukeylem6  10467  fpwwe2lem7  10590  wunfi  10674  dfnn2  12199  trclfvcotr  14975  psgnunilem3  19426  pgpfac1  20012  fiuncmp  23291  filssufilg  23798  ufileu  23806  dfn0s2  28224  pjnormssi  32097  bnj1110  34972  waj-ax  36402  bj-nnclav  36534  bj-sb  36675  bj-equsal1  36812  bj-equsal2  36813  rdgeqoa  37358  wl-mps  37495  refimssco  43596  dfbi1ALTa  44929  simprimi  44930  natlocalincr  46874  atbiffatnnb  46913  rexrsb  47101  elsetrecslem  49688