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  2569  ssorduni  7814  tz7.49  8501  nneneq  9272  nneneqOLD  9284  dfac2b  10200  qreccl  13034  dvdsaddre2b  16355  cmpsub  23429  fclsopni  24044  nocvxminlem  27840  sumdmdlem2  32451  umgr2cycllem  35108  idinside  36048  axc11n11r  36649  isbasisrelowllem1  37321  isbasisrelowllem2  37322  dmqseqim2  38613  disjlem17  38755  prtlem15  38831  prtlem17  38832  ee3bir  44474  ee233  44490  onfrALTlem2  44517  ee223  44605  ee33VD  44850  rngccatidALTV  47995  ringccatidALTV  48029