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  2564  ssorduni  7722  tz7.49  8374  nneneq  9128  dfac2b  10039  qreccl  12880  dvdsaddre2b  16232  cmpsub  23342  fclsopni  23957  nocvxminlem  27744  sumdmdlem2  32443  umgr2cycllem  35283  idinside  36227  axc11n11r  36827  isbasisrelowllem1  37499  isbasisrelowllem2  37500  dmqseqim2  38855  disjlem17  38997  prtlem15  39074  prtlem17  39075  ee3bir  44686  ee233  44702  onfrALTlem2  44729  ee223  44817  ee33VD  45061  ormkglobd  47061  rngccatidALTV  48460  ringccatidALTV  48494