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 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  a1ddd  81  com45  98  syl8ib  259  mo4  2596  ssorduni  7784  tz7.49  8438  nneneq  9197  dfac2b  10130  qreccl  13011  dvdsaddre2b  16389  cmpsub  23609  fclsopni  24225  nocvxminlem  28000  umgr2cycllem  30575  sumdmdlem2  32844  idinside  36615  axc11n11r  37367  isbasisrelowllem1  38060  isbasisrelowllem2  38061  dmqseqim2  39451  disjlem17  39611  prtlem15  39709  prtlem17  39710  ee3bir  45272  ee233  45288  onfrALTlem2  45315  ee223  45403  ee33VD  45647  ormkglobd  47651  rngccatidALTV  49096  ringccatidALTV  49130