Theorem syl3an 1313

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 1208	. 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 1002

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 1004

This theorem is referenced by:  syl2an3an  1332  funtpg  5371  ftpg  5822  eloprabga  6090  prfidisj  7085  djuenun  7390  addasspig  7513  mulasspig  7515  distrpig  7516  addcanpig  7517  mulcanpig  7518  ltapig  7521  distrnqg  7570  distrnq0  7642  cnegexlem2  8318  zletr  9492  zdivadd  9532  xaddass  10061  iooneg  10180  zltaddlt1le  10199  fzen  10235  fzaddel  10251  fzrev  10276  fzrevral2  10298  fzshftral  10300  fzosubel2  10396  fzonn0p1p1  10414  swrdf  11182  pfxccatin12lem4  11253  resqrexlemover  11516  fisum0diag2  11953  dvdsnegb  12314  muldvds1  12322  muldvds2  12323  dvdscmul  12324  dvdsmulc  12325  dvds2add  12331  dvds2sub  12332  dvdstr  12334  addmodlteqALT  12365  divalgb  12431  ndvdsadd  12437  absmulgcd  12533  rpmulgcd  12542  cncongr2  12621  hashdvds  12738  pythagtriplem1  12783  mulgmodid  13693  nmzsubg  13742