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  2427  hbae  2435  ceqsalt  3463  elabgtOLD  3615  tz7.7  6349  fvmptt  6968  f1oweALT  7925  nneneq  9140  cfcoflem  10194  nnunb  12433  ndvdssub  16378  lsmcv  21139  uvcendim  21827  gsummoncoe1  22273  2ndcsep  23424  atcvat4i  32468  mdsymlem5  32478  sumdmdii  32486  dfon2lem6  35968  colineardim1  36243  bj-hbaeb2  37125  hbae-o  39349  ax12fromc15  39351  cvrat4  39889  llncvrlpln2  40003  lplncvrlvol2  40061  dihmeetlem3N  41751  naddgeoa  43822  eel2122old  45144