Theorem syl3an 1211

Description: A triple syllogism inference. (Contributed by NM, 13-May-2004.)

Hypotheses

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

Assertion

Ref	Expression
syl3an	|- ( ( ph /\ ch /\ ta ) -> ze )

Proof of Theorem syl3an

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

Syntax hints:   -> wi 4   /\ w3a 919

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  syl2an3an  1229  funtpg  4970  ftpg  5368  eloprabga  5611  addasspig  6520  mulasspig  6522  distrpig  6523  addcanpig  6524  mulcanpig  6525  ltapig  6528  distrnqg  6577  distrnq0  6649  cnegexlem2  7284  zletr  8400  zdivadd  8436  iooneg  9010  zltaddlt1le  9028  fzen  9062  fzaddel  9077  fzrev  9101  fzrevral2  9123  fzshftral  9125  fzosubel2  9204  fzonn0p1p1  9222  resqrexlemover  9896  dvdsnegb  10212  muldvds1  10220  muldvds2  10221  dvdscmul  10222  dvdsmulc  10223  dvds2add  10229  dvds2sub  10230  dvdstr  10232  addmodlteqALT  10259  divalgb  10325  ndvdsadd  10331  absmulgcd  10406  rpmulgcd  10415  cncongr2  10486