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  2567  ssorduni  7734  tz7.49  8386  nneneq  9142  dfac2b  10053  qreccl  12894  dvdsaddre2b  16246  cmpsub  23356  fclsopni  23971  nocvxminlem  27762  sumdmdlem2  32507  umgr2cycllem  35356  idinside  36300  axc11n11r  36928  isbasisrelowllem1  37610  isbasisrelowllem2  37611  dmqseqim2  38993  disjlem17  39153  prtlem15  39251  prtlem17  39252  ee3bir  44859  ee233  44875  onfrALTlem2  44902  ee223  44990  ee33VD  45234  ormkglobd  47233  rngccatidALTV  48632  ringccatidALTV  48666