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  259  mo4  2565  ssorduni  7541  tz7.49  8159  nneneq  8807  dfac2b  9709  qreccl  12530  dvdsaddre2b  15831  cmpsub  22251  fclsopni  22866  sumdmdlem2  30454  umgr2cycllem  32769  nocvxminlem  33658  idinside  34072  axc11n11r  34551  isbasisrelowllem1  35212  isbasisrelowllem2  35213  dmqseqim2  36455  prtlem15  36575  prtlem17  36576  ee3bir  41737  ee233  41753  onfrALTlem2  41780  ee223  41868  ee33VD  42113  rngccatidALTV  45163  ringccatidALTV  45226