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  5435  ftpg  5902  eloprabga  6178  prfidisj  7240  djuenun  7574  addasspig  7703  mulasspig  7705  distrpig  7706  addcanpig  7707  mulcanpig  7708  ltapig  7711  distrnqg  7760  distrnq0  7832  cnegexlem2  8509  zletr  9703  zdivadd  9745  xaddass  10287  iooneg  10406  zltaddlt1le  10426  fzen  10463  fzaddel  10481  fzrev  10507  fzrevral2  10529  fzshftral  10531  fzosubel2  10629  fzonn0p1p1  10647  swrdf  11448  pfxccatin12lem4  11519  resqrexlemover  11797  fisum0diag2  12238  dvdsnegb  12599  muldvds1  12607  muldvds2  12608  dvdscmul  12609  dvdsmulc  12610  dvds2add  12616  dvds2sub  12617  dvdstr  12619  addmodlteqALT  12650  divalgb  12716  ndvdsadd  12722  absmulgcd  12818  rpmulgcd  12827  cncongr2  12906  hashdvds  13027  pythagtriplem1  13072  mulgmodid  14022  nmzsubg  14071  assa2ass  15117  psrbagconf1o  15177  gsumbagdiaglem  15184  psrass1filem  15186  psrass1fi  15210  clwwlknccat  16886