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  254  ax12  2425  hbae  2433  tz7.7  6291  fvmptt  6892  f1oweALT  7808  wfrlem12OLD  8142  nneneq  8973  nneneqOLD  8986  pr2nelem  9761  cfcoflem  10029  nnunb  12229  ndvdssub  16116  lsmcv  20401  uvcendim  21052  gsummoncoe1  21473  2ndcsep  22608  atcvat4i  30755  mdsymlem5  30765  sumdmdii  30773  dfon2lem6  33760  colineardim1  34359  bj-hbaeb2  34997  hbae-o  36913  ax12fromc15  36915  cvrat4  37453  llncvrlpln2  37567  lplncvrlvol2  37625  dihmeetlem3N  39315  eel2122old  42308