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  255  mo4  2566  ssorduni  7606  tz7.49  8246  nneneq  8896  dfac2b  9817  qreccl  12638  dvdsaddre2b  15944  cmpsub  22459  fclsopni  23074  sumdmdlem2  30682  umgr2cycllem  33002  nocvxminlem  33899  idinside  34313  axc11n11r  34792  isbasisrelowllem1  35453  isbasisrelowllem2  35454  dmqseqim2  36696  prtlem15  36816  prtlem17  36817  ee3bir  42012  ee233  42028  onfrALTlem2  42055  ee223  42143  ee33VD  42388  rngccatidALTV  45435  ringccatidALTV  45498