Theorem syl3an 628

Description: A triple syllogism inference.

Hypotheses

Ref	Expression
syl3an.1	|- ((ph /\ ps /\ ch) -> th)
syl3an.2	|- (ta -> ph)
syl3an.3	|- (et -> ps)
syl3an.4	|- (ze -> ch)

Assertion

Ref	Expression
syl3an	|- ((ta /\ et /\ ze) -> th)

Proof of Theorem syl3an

Step	Hyp	Ref	Expression
1		syl3an.2	. . 3 |- (ta -> ph)
2		syl3an.3	. . 3 |- (et -> ps)
3		syl3an.4	. . 3 |- (ze -> ch)
4	1, 2, 3	im3an 605	. 2 |- ((ta /\ et /\ ze) -> (ph /\ ps /\ ch))
5		syl3an.1	. 2 |- ((ph /\ ps /\ ch) -> th)
6	4, 5	syl 12	1 |- ((ta /\ et /\ ze) -> th)

Syntax hints:   -> wi 2   /\ w3a 581

This theorem is referenced by:  tpss 1855  fr3nr 2178  nnaord 3177  nnaass 3179  nnacan 3184  nnaword 3185  addasspi 3817  mulasspi 3819  distrpi 3820  mulcanpi 3821  ltapi 3824  lesub1t 4352  qbtwnre 4650  shmods 5363  chlej1t 5427  chlej2t 5428  atexch 5769  atcvatlem 5770  sumdmdi 5785  sumdmdlem 5786

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198  df-3an 583

metamath.org