Theorem syl3an 1216

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 1128	. 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 924

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 926

This theorem is referenced by:  syl2an3an  1234  funtpg  5065  ftpg  5481  eloprabga  5735  prfidisj  6635  addasspig  6887  mulasspig  6889  distrpig  6890  addcanpig  6891  mulcanpig  6892  ltapig  6895  distrnqg  6944  distrnq0  7016  cnegexlem2  7656  zletr  8797  zdivadd  8833  iooneg  9403  zltaddlt1le  9421  fzen  9455  fzaddel  9470  fzrev  9494  fzrevral2  9516  fzshftral  9518  fzosubel2  9602  fzonn0p1p1  9620  resqrexlemover  10439  fisum0diag2  10837  dvdsnegb  11087  muldvds1  11095  muldvds2  11096  dvdscmul  11097  dvdsmulc  11098  dvds2add  11104  dvds2sub  11105  dvdstr  11107  addmodlteqALT  11134  divalgb  11199  ndvdsadd  11205  absmulgcd  11280  rpmulgcd  11289  cncongr2  11360  hashdvds  11471