Theorem syl3an 1292

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 1187	. 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 981

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

This theorem depends on definitions:  df-bi 117  df-3an 983

This theorem is referenced by:  syl2an3an  1311  funtpg  5339  ftpg  5786  eloprabga  6050  prfidisj  7045  djuenun  7350  addasspig  7473  mulasspig  7475  distrpig  7476  addcanpig  7477  mulcanpig  7478  ltapig  7481  distrnqg  7530  distrnq0  7602  cnegexlem2  8278  zletr  9452  zdivadd  9492  xaddass  10021  iooneg  10140  zltaddlt1le  10159  fzen  10195  fzaddel  10211  fzrev  10236  fzrevral2  10258  fzshftral  10260  fzosubel2  10356  fzonn0p1p1  10374  swrdf  11141  resqrexlemover  11406  fisum0diag2  11843  dvdsnegb  12204  muldvds1  12212  muldvds2  12213  dvdscmul  12214  dvdsmulc  12215  dvds2add  12221  dvds2sub  12222  dvdstr  12224  addmodlteqALT  12255  divalgb  12321  ndvdsadd  12327  absmulgcd  12423  rpmulgcd  12432  cncongr2  12511  hashdvds  12628  pythagtriplem1  12673  mulgmodid  13582  nmzsubg  13631