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  2561  ssorduni  7712  tz7.49  8364  nneneq  9115  dfac2b  10022  qreccl  12867  dvdsaddre2b  16218  cmpsub  23315  fclsopni  23930  nocvxminlem  27717  sumdmdlem2  32399  umgr2cycllem  35184  idinside  36128  axc11n11r  36727  isbasisrelowllem1  37399  isbasisrelowllem2  37400  dmqseqim2  38765  disjlem17  38907  prtlem15  38984  prtlem17  38985  ee3bir  44606  ee233  44622  onfrALTlem2  44649  ee223  44737  ee33VD  44981  ormkglobd  46983  rngccatidALTV  48382  ringccatidALTV  48416