Theorem syl3an 1270

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 1174	. 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 968

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 970

This theorem is referenced by:  syl2an3an  1288  funtpg  5238  ftpg  5668  eloprabga  5925  prfidisj  6888  djuenun  7164  addasspig  7267  mulasspig  7269  distrpig  7270  addcanpig  7271  mulcanpig  7272  ltapig  7275  distrnqg  7324  distrnq0  7396  cnegexlem2  8070  zletr  9236  zdivadd  9276  xaddass  9801  iooneg  9920  zltaddlt1le  9939  fzen  9974  fzaddel  9990  fzrev  10015  fzrevral2  10037  fzshftral  10039  fzosubel2  10126  fzonn0p1p1  10144  resqrexlemover  10948  fisum0diag2  11384  dvdsnegb  11744  muldvds1  11752  muldvds2  11753  dvdscmul  11754  dvdsmulc  11755  dvds2add  11761  dvds2sub  11762  dvdstr  11764  addmodlteqALT  11793  divalgb  11858  ndvdsadd  11864  absmulgcd  11946  rpmulgcd  11955  cncongr2  12032  hashdvds  12149  pythagtriplem1  12193