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  2559  ssorduni  7715  tz7.49  8367  nneneq  9120  dfac2b  10025  qreccl  12870  dvdsaddre2b  16218  cmpsub  23285  fclsopni  23900  nocvxminlem  27688  sumdmdlem2  32363  umgr2cycllem  35117  idinside  36062  axc11n11r  36661  isbasisrelowllem1  37333  isbasisrelowllem2  37334  dmqseqim2  38639  disjlem17  38781  prtlem15  38858  prtlem17  38859  ee3bir  44481  ee233  44497  onfrALTlem2  44524  ee223  44612  ee33VD  44856  ormkglobd  46860  rngccatidALTV  48260  ringccatidALTV  48294