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  123  ancl  528  ancr  530  anc2r  538  hbim1  2289  hbim1OLD  2389  ralimia  3099  ceqsalgALT  3383  rspct  3454  elabgt  3499  fvmptt  6443  tfi  7201  fnfi  8395  finsschain  8430  ordiso2  8577  ordtypelem7  8586  dfom3  8709  infdiffi  8720  cantnfp1lem3  8742  cantnf  8755  r1ordg  8806  ttukeylem6  9539  fpwwe2lem8  9662  wunfi  9746  dfnn2  11236  trclfvcotr  13959  psgnunilem3  18124  pgpfac1  18688  fiuncmp  21429  filssufilg  21936  ufileu  21944  pjnormssi  29368  bnj1110  31389  waj-ax  32751  bj-sb  33015  bj-equsal1  33147  bj-equsal2  33148  rdgeqoa  33556  wl-mps  33628  refimssco  38440  atbiffatnnb  41600  elsetrecslem  42974