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  7735  tz7.49  8390  nneneq  9147  dfac2b  10060  qreccl  12904  dvdsaddre2b  16253  cmpsub  23263  fclsopni  23878  nocvxminlem  27665  sumdmdlem2  32321  umgr2cycllem  35100  idinside  36045  axc11n11r  36644  isbasisrelowllem1  37316  isbasisrelowllem2  37317  dmqseqim2  38622  disjlem17  38764  prtlem15  38841  prtlem17  38842  ee3bir  44466  ee233  44482  onfrALTlem2  44509  ee223  44597  ee33VD  44841  ormkglobd  46846  rngccatidALTV  48233  ringccatidALTV  48267