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  2163  hbim1OLD  2263  ralimia  2979  ceqsalgALT  3262  rspct  3333  elabgt  3379  fvmptt  6339  tfi  7095  fnfi  8279  finsschain  8314  ordiso2  8461  ordtypelem7  8470  dfom3  8582  infdiffi  8593  cantnfp1lem3  8615  cantnf  8628  r1ordg  8679  ttukeylem6  9374  fpwwe2lem8  9497  wunfi  9581  dfnn2  11071  trclfvcotr  13794  psgnunilem3  17962  pgpfac1  18525  fiuncmp  21255  filssufilg  21762  ufileu  21770  pjnormssi  29155  bnj1110  31176  waj-ax  32538  bj-sb  32802  bj-equsal1  32936  bj-equsal2  32937  rdgeqoa  33348  wl-mps  33420  refimssco  38230  atbiffatnnb  41400  elsetrecslem  42770