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 )

Syntax hints:   -> wi 4   /\ w3a 1009

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 1011

This theorem is referenced by:  syl2an3an  1339  funtpg  5427  ftpg  5890  eloprabga  6165  prfidisj  7224  djuenun  7558  addasspig  7687  mulasspig  7689  distrpig  7690  addcanpig  7691  mulcanpig  7692  ltapig  7695  distrnqg  7744  distrnq0  7816  cnegexlem2  8492  zletr  9673  zdivadd  9714  xaddass  10250  iooneg  10369  zltaddlt1le  10389  fzen  10426  fzaddel  10443  fzrev  10469  fzrevral2  10491  fzshftral  10493  fzosubel2  10591  fzonn0p1p1  10609  swrdf  11405  pfxccatin12lem4  11476  resqrexlemover  11754  fisum0diag2  12192  dvdsnegb  12553  muldvds1  12561  muldvds2  12562  dvdscmul  12563  dvdsmulc  12564  dvds2add  12570  dvds2sub  12571  dvdstr  12573  addmodlteqALT  12604  divalgb  12670  ndvdsadd  12676  absmulgcd  12772  rpmulgcd  12781  cncongr2  12860  hashdvds  12977  pythagtriplem1  13022  mulgmodid  13941  nmzsubg  13990  psrbagconf1o  14987  clwwlknccat  16578