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  38754  disjlem17  38896  prtlem15  38973  prtlem17  38974  ee3bir  44595  ee233  44611  onfrALTlem2  44638  ee223  44726  ee33VD  44970  ormkglobd  46972  rngccatidALTV  48371  ringccatidALTV  48405