Theorem syl3an 1275

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 1179	. 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 973

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

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  syl2an3an  1293  funtpg  5249  ftpg  5680  eloprabga  5940  prfidisj  6904  djuenun  7189  addasspig  7292  mulasspig  7294  distrpig  7295  addcanpig  7296  mulcanpig  7297  ltapig  7300  distrnqg  7349  distrnq0  7421  cnegexlem2  8095  zletr  9261  zdivadd  9301  xaddass  9826  iooneg  9945  zltaddlt1le  9964  fzen  9999  fzaddel  10015  fzrev  10040  fzrevral2  10062  fzshftral  10064  fzosubel2  10151  fzonn0p1p1  10169  resqrexlemover  10974  fisum0diag2  11410  dvdsnegb  11770  muldvds1  11778  muldvds2  11779  dvdscmul  11780  dvdsmulc  11781  dvds2add  11787  dvds2sub  11788  dvdstr  11790  addmodlteqALT  11819  divalgb  11884  ndvdsadd  11890  absmulgcd  11972  rpmulgcd  11981  cncongr2  12058  hashdvds  12175  pythagtriplem1  12219