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  258  mo4  2650  ssorduni  7502  tz7.49  8083  nneneq  8702  dfac2b  9558  qreccl  12371  dvdsaddre2b  15659  cmpsub  22010  fclsopni  22625  sumdmdlem2  30198  umgr2cycllem  32389  nocvxminlem  33249  idinside  33547  axc11n11r  34019  isbasisrelowllem1  34638  isbasisrelowllem2  34639  dmqseqim2  35893  prtlem15  36013  prtlem17  36014  ee3bir  40844  ee233  40860  onfrALTlem2  40887  ee223  40975  ee33VD  41220  rngccatidALTV  44267  ringccatidALTV  44330