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  546  ancr  548  anc2r  556  hbim1  2294  ralimia  3081  ceqsalgALT  3509  rspct  3599  elabgtOLD  3664  fvmptt  7019  tfi  7842  imafi  9175  fnfi  9181  finsschain  9359  ordiso2  9510  ordtypelem7  9519  dfom3  9642  infdiffi  9653  cantnfp1lem3  9675  cantnf  9688  r1ordg  9773  ttukeylem6  10509  fpwwe2lem7  10632  wunfi  10716  dfnn2  12225  trclfvcotr  14956  psgnunilem3  19364  pgpfac1  19950  fiuncmp  22908  filssufilg  23415  ufileu  23423  pjnormssi  31421  bnj1110  33993  waj-ax  35299  bj-nnclav  35422  bj-sb  35565  bj-equsal1  35702  bj-equsal2  35703  rdgeqoa  36251  wl-mps  36376  refimssco  42358  natlocalincr  45590  atbiffatnnb  45622  rexrsb  45808  elsetrecslem  47744