Theorem syl7 74

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 73	1 ⊢ (𝜒 → (𝜃 → (𝜑 → 𝜏)))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  syl7bi  255  ax12  2421  hbae  2429  ceqsalt  3470  elabgtOLD  3628  tz7.7  6333  fvmptt  6950  f1oweALT  7907  nneneq  9120  cfcoflem  10166  nnunb  12380  ndvdssub  16320  lsmcv  21048  uvcendim  21754  gsummoncoe1  22193  2ndcsep  23344  atcvat4i  32341  mdsymlem5  32351  sumdmdii  32359  dfon2lem6  35766  colineardim1  36039  bj-hbaeb2  36796  hbae-o  38886  ax12fromc15  38888  cvrat4  39426  llncvrlpln2  39540  lplncvrlvol2  39598  dihmeetlem3N  41288  naddgeoa  43371  eel2122old  44695