MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl3an Unicode version

Theorem syl3an 1224
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 1137 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  ( ps  /\  th 
/\  et ) )
5 syl3an.4 . 2  |-  ( ( ps  /\  th  /\  et )  ->  ze )
64, 5syl 15 1  |-  ( (
ph  /\  ch  /\  ta )  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  fresaun  5412  fresaunres2  5413  eloprabga  5934  cdaenun  7800  addasspi  8519  mulasspi  8521  distrpi  8522  addcanpi  8523  mulcanpi  8524  ltapi  8527  lemul1  9608  ltdiv2  9641  zdivadd  10083  uztrn  10244  uzss  10248  qdivcl  10337  maxle  10519  lemin  10520  maxlt  10521  ltmin  10522  xaddass  10569  xmulasslem3  10606  xadddilem  10614  iooneg  10756  fzen  10811  fzaddel  10826  fzrev  10846  fzrevral2  10867  fzshftral  10869  fzosubel2  10909  fldiv2  10965  modmulnn  10988  modcyc2  11000  hashssdif  11374  fsum0diag2  12245  efsub  12380  dvdsnegb  12546  muldvds1  12553  muldvds2  12554  dvdscmul  12555  dvdsmulc  12556  dvdscmulr  12557  dvdsmulcr  12558  dvds2add  12560  dvds2sub  12561  dvdstr  12562  divalglem8  12599  divalgb  12603  divalgmod  12605  ndvdsadd  12607  modgcd  12715  absmulgcd  12726  rpmulgcd  12734  hashdvds  12843  pythagtriplem1  12869  vdwlem3  13030  ressinbas  13204  gsumws2  14465  nmzsubg  14658  subcmn  15133  gexexlem  15144  lsmcom  15150  zaddablx  15160  psrbagconf1o  16120  gsumbagdiaglem  16121  psrass1lem  16123  psrass1  16150  mplmonmul  16208  ply1opprmul  16317  coe1mul  16347  2ndcdisj2  17183  fbssfi  17532  isfcf  17729  nmotri  18248  nghmplusg  18249  0nmhm  18264  iundisj2  18906  ovolioo  18925  uniiccdif  18933  basellem9  20326  gxmodid  20946  issubgoi  20977  ablomul  21022  lnocoi  21335  ipasslem5  21413  hhssnv  21841  shscli  21896  shmodsi  21968  lnopmi  22580  lnopcoi  22583  cnlnadjlem2  22648  adjmul  22672  leopmul2i  22715  leoptr  22717  pjimai  22756  mdslle1i  22897  mdslle2i  22898  mdslj1i  22899  mdslj2i  22900  mdslmd1lem1  22905  mdslmd2i  22910  atexch  22961  atcvatlem  22965  chirredlem3  22972  sumdmdii  22995  sumdmdlem  22998  cdj3i  23021  iundisj2fi  23364  iundisj2f  23366  cgr3permute3  24670  cgr3permute1  24671  cgr3com  24676  nndivsub  24896  injsurinj  25149  cnvtr  25616  rnegvex2  25661  negveudr  25669  subclrvd  25674  clsmulrv  25683  divclrvd  25695  1cat  25759  fzmul  26443  fzadd2  26444  lpss2  26468  isismty  26525  heibor1  26534  heiborlem3  26537  elmapresaun  26850  elmapresaunres2  26851  fzneg  27069  lsmfgcl  27172  psgnghm  27437  trelded  28331  jaoded  28332  eel112  28477  el123  28539  suctrALTcf  28698  suctrALT4  28704  bnj1384  29062  hlatjcl  29556  hlatjcom  29557  hlatlej1  29564  hlrelat5N  29590  2lplnmN  29748  2llnmj  29749  2lplnmj  29811
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator