Theorem syl8 74

Description: A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 1-Aug-1994.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)

Hypotheses

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

Assertion

Ref	Expression
syl8	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))

Proof of Theorem syl8

Step	Hyp	Ref	Expression
1		syl8.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2		syl8.2	. . 3 ⊢ (𝜃 → 𝜏)
3	2	a1i 11	. 2 ⊢ (𝜑 → (𝜃 → 𝜏))
4	1, 3	syl6d 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:  a1ddd  78  com45  95  syl8ib  245  imp5a  622  3exp  1256  3imp3i2an  1270  suctrOLD  5726  ssorduni  6877  tfindsg  6952  findsg  6985  tz7.49  7427  nneneq  8028  dfac2  8836  qreccl  11684  dvdsaddre2b  14867  cmpsub  21013  fclsopni  21629  wlkdvspthlem  26137  sumdmdlem2  28662  nocvxminlem  31089  idinside  31361  axc11n11r  31860  bj-nfimt  32025  isbasisrelowllem1  32379  isbasisrelowllem2  32380  prtlem15  33178  prtlem17  33179  ee3bir  37730  ee233  37746  onfrALTlem2  37782  ee223  37880  ee33VD  38137  rngccatidALTV  41781  ringccatidALTV  41844