Theorem syl7 75

Description: A syllogism rule of inference. The first premise is used to replace the third antecedent of the second premise. (Contributed by NM, 12-Jan-1993.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)

Hypotheses

Ref	Expression
syl7.1	⊢ (𝜑 → 𝜓)
syl7.2	⊢ (𝜒 → (𝜃 → (𝜓 → 𝜏)))

Assertion

Ref	Expression
syl7	⊢ (𝜒 → (𝜃 → (𝜑 → 𝜏)))

Proof of Theorem syl7

Step	Hyp	Ref	Expression
1		syl7.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1i 11	. 2 ⊢ (𝜒 → (𝜑 → 𝜓))
3		syl7.2	. 2 ⊢ (𝜒 → (𝜃 → (𝜓 → 𝜏)))
4	2, 3	syl5d 74	1 ⊢ (𝜒 → (𝜃 → (𝜑 → 𝜏)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syl7bi  258  ax12  2454  hbae  2462  ceqsalt  3486  elabgtOLD  3630  tz7.7  6387  fvmptt  7011  f1oweALT  7973  nneneq  9204  cfcoflem  10278  nnunb  12528  ndvdssub  16505  lsmcv  21334  uvcendim  22066  gsummoncoe1  22539  2ndcsep  23691  atcvat4i  32886  mdsymlem5  32896  sumdmdii  32904  axsepg4  35677  dfon2lem6  36373  colineardim1  36649  bj-hbaeb2  37569  hbae-o  39784  ax12fromc15  39786  cvrat4  40324  llncvrlpln2  40438  lplncvrlvol2  40496  dihmeetlem3N  42186  naddgeoa  44243  eel2122old  45548