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  2559  ssorduni  7755  tz7.49  8413  nneneq  9170  dfac2b  10084  qreccl  12928  dvdsaddre2b  16277  cmpsub  23287  fclsopni  23902  nocvxminlem  27689  sumdmdlem2  32348  umgr2cycllem  35127  idinside  36072  axc11n11r  36671  isbasisrelowllem1  37343  isbasisrelowllem2  37344  dmqseqim2  38649  disjlem17  38791  prtlem15  38868  prtlem17  38869  ee3bir  44493  ee233  44509  onfrALTlem2  44536  ee223  44624  ee33VD  44868  ormkglobd  46873  rngccatidALTV  48260  ringccatidALTV  48294