Theorem syl3an 1291

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 1186	. 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 980

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 982

This theorem is referenced by:  syl2an3an  1310  funtpg  5324  ftpg  5767  eloprabga  6031  prfidisj  7023  djuenun  7323  addasspig  7442  mulasspig  7444  distrpig  7445  addcanpig  7446  mulcanpig  7447  ltapig  7450  distrnqg  7499  distrnq0  7571  cnegexlem2  8247  zletr  9421  zdivadd  9461  xaddass  9990  iooneg  10109  zltaddlt1le  10128  fzen  10164  fzaddel  10180  fzrev  10205  fzrevral2  10227  fzshftral  10229  fzosubel2  10322  fzonn0p1p1  10340  resqrexlemover  11263  fisum0diag2  11700  dvdsnegb  12061  muldvds1  12069  muldvds2  12070  dvdscmul  12071  dvdsmulc  12072  dvds2add  12078  dvds2sub  12079  dvdstr  12081  addmodlteqALT  12112  divalgb  12178  ndvdsadd  12184  absmulgcd  12280  rpmulgcd  12289  cncongr2  12368  hashdvds  12485  pythagtriplem1  12530  mulgmodid  13439  nmzsubg  13488