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  2560  ssorduni  7758  tz7.49  8416  nneneq  9176  dfac2b  10091  qreccl  12935  dvdsaddre2b  16284  cmpsub  23294  fclsopni  23909  nocvxminlem  27696  sumdmdlem2  32355  umgr2cycllem  35134  idinside  36079  axc11n11r  36678  isbasisrelowllem1  37350  isbasisrelowllem2  37351  dmqseqim2  38656  disjlem17  38798  prtlem15  38875  prtlem17  38876  ee3bir  44500  ee233  44516  onfrALTlem2  44543  ee223  44631  ee33VD  44875  ormkglobd  46880  rngccatidALTV  48264  ringccatidALTV  48298