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  2431  hbae  2439  ceqsalt  3523  elabgt  3685  tz7.7  6421  fvmptt  7049  f1oweALT  8013  wfrlem12OLD  8376  nneneq  9272  nneneqOLD  9284  pr2nelemOLD  10072  cfcoflem  10341  nnunb  12549  ndvdssub  16457  lsmcv  21166  uvcendim  21890  gsummoncoe1  22333  2ndcsep  23488  atcvat4i  32429  mdsymlem5  32439  sumdmdii  32447  dfon2lem6  35752  colineardim1  36025  bj-hbaeb2  36784  hbae-o  38859  ax12fromc15  38861  cvrat4  39400  llncvrlpln2  39514  lplncvrlvol2  39572  dihmeetlem3N  41262  naddgeoa  43356  eel2122old  44689