Theorem syl8 77

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 76	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  81  com45  98  syl8ib  259  mo4  2600  ssorduni  7778  tz7.49  8432  nneneq  9190  dfac2b  10114  qreccl  12993  dvdsaddre2b  16365  cmpsub  23526  fclsopni  24141  nocvxminlem  27913  sumdmdlem2  32712  umgr2cycllem  35531  idinside  36475  axc11n11r  37197  isbasisrelowllem1  37889  isbasisrelowllem2  37890  dmqseqim2  39281  disjlem17  39441  prtlem15  39539  prtlem17  39540  ee3bir  45104  ee233  45120  onfrALTlem2  45147  ee223  45235  ee33VD  45479  ormkglobd  47483  rngccatidALTV  48926  ringccatidALTV  48960