Theorem syl8 76

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 75	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  80  com45  97  syl8ib  257  mo4  2609  ssorduni  7363  tz7.49  7939  nneneq  8554  dfac2b  9409  qreccl  12222  dvdsaddre2b  15494  cmpsub  21696  fclsopni  22311  sumdmdlem2  29883  umgr2cycllem  31997  nocvxminlem  32858  idinside  33156  axc11n11r  33621  isbasisrelowllem1  34188  isbasisrelowllem2  34189  dmqseqim2  35443  prtlem15  35563  prtlem17  35564  ee3bir  40397  ee233  40413  onfrALTlem2  40440  ee223  40528  ee33VD  40773  rngccatidALTV  43760  ringccatidALTV  43823