Theorem syl3an 1320

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 1215	. 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 )

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  syl2an3an  1339  funtpg  5432  ftpg  5899  eloprabga  6175  prfidisj  7234  djuenun  7568  addasspig  7697  mulasspig  7699  distrpig  7700  addcanpig  7701  mulcanpig  7702  ltapig  7705  distrnqg  7754  distrnq0  7826  cnegexlem2  8502  zletr  9694  zdivadd  9735  xaddass  10271  iooneg  10390  zltaddlt1le  10410  fzen  10447  fzaddel  10465  fzrev  10491  fzrevral2  10513  fzshftral  10515  fzosubel2  10613  fzonn0p1p1  10631  swrdf  11427  pfxccatin12lem4  11498  resqrexlemover  11776  fisum0diag2  12214  dvdsnegb  12575  muldvds1  12583  muldvds2  12584  dvdscmul  12585  dvdsmulc  12586  dvds2add  12592  dvds2sub  12593  dvdstr  12595  addmodlteqALT  12626  divalgb  12692  ndvdsadd  12698  absmulgcd  12794  rpmulgcd  12803  cncongr2  12882  hashdvds  12999  pythagtriplem1  13044  mulgmodid  13964  nmzsubg  14013  assa2ass  15009  psrbagconf1o  15064  clwwlknccat  16664