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  256  mo4  2565  ssorduni  7771  tz7.49  8457  nneneq  9218  dfac2b  10143  qreccl  12983  dvdsaddre2b  16324  cmpsub  23336  fclsopni  23951  nocvxminlem  27739  sumdmdlem2  32346  umgr2cycllem  35108  idinside  36048  axc11n11r  36647  isbasisrelowllem1  37319  isbasisrelowllem2  37320  dmqseqim2  38621  disjlem17  38763  prtlem15  38839  prtlem17  38840  ee3bir  44476  ee233  44492  onfrALTlem2  44519  ee223  44607  ee33VD  44851  ormkglobd  46852  rngccatidALTV  48195  ringccatidALTV  48229