ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl3an Unicode version

Theorem syl3an 1262
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
StepHypRef Expression
1 syl3an.1 . . 3  |-  ( ph  ->  ps )
2 syl3an.2 . . 3  |-  ( ch 
->  th )
3 syl3an.3 . . 3  |-  ( ta 
->  et )
41, 2, 33anim123i 1167 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  ( ps  /\  th 
/\  et ) )
5 syl3an.4 . 2  |-  ( ( ps  /\  th  /\  et )  ->  ze )
64, 5syl 14 1  |-  ( (
ph  /\  ch  /\  ta )  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 963
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 965
This theorem is referenced by:  syl2an3an  1280  funtpg  5223  ftpg  5653  eloprabga  5910  prfidisj  6873  djuenun  7149  addasspig  7252  mulasspig  7254  distrpig  7255  addcanpig  7256  mulcanpig  7257  ltapig  7260  distrnqg  7309  distrnq0  7381  cnegexlem2  8055  zletr  9221  zdivadd  9258  xaddass  9779  iooneg  9898  zltaddlt1le  9917  fzen  9951  fzaddel  9967  fzrev  9992  fzrevral2  10014  fzshftral  10016  fzosubel2  10103  fzonn0p1p1  10121  resqrexlemover  10921  fisum0diag2  11355  dvdsnegb  11715  muldvds1  11723  muldvds2  11724  dvdscmul  11725  dvdsmulc  11726  dvds2add  11732  dvds2sub  11733  dvdstr  11735  addmodlteqALT  11763  divalgb  11828  ndvdsadd  11834  absmulgcd  11916  rpmulgcd  11925  cncongr2  11996  hashdvds  12111  pythagtriplem1  12155
  Copyright terms: Public domain W3C validator