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  5430  ftpg  5893  eloprabga  6168  prfidisj  7227  djuenun  7561  addasspig  7690  mulasspig  7692  distrpig  7693  addcanpig  7694  mulcanpig  7695  ltapig  7698  distrnqg  7747  distrnq0  7819  cnegexlem2  8495  zletr  9676  zdivadd  9717  xaddass  10253  iooneg  10372  zltaddlt1le  10392  fzen  10429  fzaddel  10446  fzrev  10472  fzrevral2  10494  fzshftral  10496  fzosubel2  10594  fzonn0p1p1  10612  swrdf  11408  pfxccatin12lem4  11479  resqrexlemover  11757  fisum0diag2  12195  dvdsnegb  12556  muldvds1  12564  muldvds2  12565  dvdscmul  12566  dvdsmulc  12567  dvds2add  12573  dvds2sub  12574  dvdstr  12576  addmodlteqALT  12607  divalgb  12673  ndvdsadd  12679  absmulgcd  12775  rpmulgcd  12784  cncongr2  12863  hashdvds  12980  pythagtriplem1  13025  mulgmodid  13944  nmzsubg  13993  psrbagconf1o  14990  clwwlknccat  16581