Theorem syl3an 1258

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 1166	. 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 962

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

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  syl2an3an  1276  funtpg  5174  ftpg  5604  eloprabga  5858  prfidisj  6815  djuenun  7068  addasspig  7138  mulasspig  7140  distrpig  7141  addcanpig  7142  mulcanpig  7143  ltapig  7146  distrnqg  7195  distrnq0  7267  cnegexlem2  7938  zletr  9103  zdivadd  9140  xaddass  9652  iooneg  9771  zltaddlt1le  9789  fzen  9823  fzaddel  9839  fzrev  9864  fzrevral2  9886  fzshftral  9888  fzosubel2  9972  fzonn0p1p1  9990  resqrexlemover  10782  fisum0diag2  11216  dvdsnegb  11510  muldvds1  11518  muldvds2  11519  dvdscmul  11520  dvdsmulc  11521  dvds2add  11527  dvds2sub  11528  dvdstr  11530  addmodlteqALT  11557  divalgb  11622  ndvdsadd  11628  absmulgcd  11705  rpmulgcd  11714  cncongr2  11785  hashdvds  11897