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  7629  tz7.49  8276  nneneq  8992  nneneqOLD  9004  dfac2b  9886  qreccl  12709  dvdsaddre2b  16016  cmpsub  22551  fclsopni  23166  sumdmdlem2  30781  umgr2cycllem  33102  nocvxminlem  33972  idinside  34386  axc11n11r  34865  isbasisrelowllem1  35526  isbasisrelowllem2  35527  dmqseqim2  36769  prtlem15  36889  prtlem17  36890  ee3bir  42123  ee233  42139  onfrALTlem2  42166  ee223  42254  ee33VD  42499  rngccatidALTV  45547  ringccatidALTV  45610