Theorem syl8 77

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 76	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  81  com45  98  syl8ib  259  mo4  2594  ssorduni  7774  tz7.49  8428  nneneq  9186  dfac2b  10110  qreccl  12988  dvdsaddre2b  16360  cmpsub  23557  fclsopni  24172  nocvxminlem  27947  sumdmdlem2  32771  umgr2cycllem  35632  idinside  36576  axc11n11r  37328  isbasisrelowllem1  38021  isbasisrelowllem2  38022  dmqseqim2  39411  disjlem17  39571  prtlem15  39669  prtlem17  39670  ee3bir  45232  ee233  45248  onfrALTlem2  45275  ee223  45363  ee33VD  45607  ormkglobd  47611  rngccatidALTV  49057  ringccatidALTV  49091