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  2563  ssorduni  7797  tz7.49  8483  nneneq  9243  nneneqOLD  9255  dfac2b  10168  qreccl  13008  dvdsaddre2b  16340  cmpsub  23423  fclsopni  24038  nocvxminlem  27836  sumdmdlem2  32447  umgr2cycllem  35124  idinside  36065  axc11n11r  36665  isbasisrelowllem1  37337  isbasisrelowllem2  37338  dmqseqim2  38638  disjlem17  38780  prtlem15  38856  prtlem17  38857  ee3bir  44500  ee233  44516  onfrALTlem2  44543  ee223  44631  ee33VD  44876  rngccatidALTV  48115  ringccatidALTV  48149