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

Theorem syl3an 1261
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 1173 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  ( ps  /\  th 
/\  et ) )
5 syl3an.4 . 2  |-  ( ( ps  /\  th  /\  et )  ->  ze )
64, 5syl 16 1  |-  ( (
ph  /\  ch  /\  ta )  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967
This theorem is referenced by:  funtpg  5566  fresaun  5680  fresaunres2  5681  ftpg  5991  eloprabga  6277  cdaenun  8444  addasspi  9165  mulasspi  9167  distrpi  9168  addcanpi  9169  mulcanpi  9170  ltapi  9173  lemul1  10282  ltdiv2  10318  zletr  10790  zdivadd  10814  uztrn  10978  uzss  10982  qdivcl  11075  maxle  11263  lemin  11264  maxlt  11265  ltmin  11266  xaddass  11313  xmulasslem3  11350  xadddilem  11358  iooneg  11506  fzen  11568  fzaddel  11594  fzrev  11620  fzrevral2  11646  fzshftral  11648  fzosubel2  11701  fldiv2  11801  modmulnn  11826  modcyc2  11845  hashssdif  12269  ccatsymb  12383  ccatw2s1ass  12410  swrdccatin12lem1  12477  fsum0diag2  13352  efsub  13486  dvdsnegb  13652  muldvds1  13659  muldvds2  13660  dvdscmul  13661  dvdsmulc  13662  dvdscmulr  13663  dvdsmulcr  13664  dvds2add  13666  dvds2sub  13667  dvdstr  13668  divalglem8  13706  divalgb  13710  divalgmod  13712  ndvdsadd  13714  modgcd  13822  absmulgcd  13833  rpmulgcd  13841  hashdvds  13952  pythagtriplem1  13985  vdwlem3  14146  ressinbas  14336  gsumws2  15622  nmzsubg  15824  pmtr3ncomlem1  16081  pmtrdifellem1  16084  subcmn  16425  gexexlem  16438  lsmcom  16444  zaddablx  16454  psrbagconf1o  17550  gsumbagdiaglem  17551  psrass1lem  17553  psrass1  17584  mplmonmul  17650  ply1opprmul  17801  coe1mul  17831  psgnghm  18119  2ndcdisj2  19177  fbssfi  19526  isfcf  19723  nmotri  20434  nghmplusg  20435  0nmhm  20450  iundisj2  21146  ovolioo  21165  uniiccdif  21174  basellem9  22542  nb3grapr  23496  gxmodid  23901  issubgoi  23932  ablomul  23977  lnocoi  24292  ipasslem5  24370  hhssnv  24800  shscli  24855  shmodsi  24927  lnopmi  25539  lnopcoi  25542  cnlnadjlem2  25607  adjmul  25631  leopmul2i  25674  leoptr  25676  pjimai  25715  mdslle1i  25856  mdslle2i  25857  mdslj1i  25858  mdslj2i  25859  mdslmd1lem1  25864  mdslmd2i  25869  atexch  25920  atcvatlem  25924  chirredlem3  25931  sumdmdii  25954  sumdmdlem  25957  cdj3i  25980  iundisj2f  26066  iundisj2fi  26215  xrge0omnd  26308  binomrisefac  27679  cgr3permute3  28212  cgr3permute1  28213  cgr3com  28218  nndivsub  28437  mblfinlem2  28567  cnambfre  28578  ftc1anclem5  28609  fzmul  28774  fzadd2  28775  isismty  28838  heibor1  28847  heiborlem3  28850  elmapresaun  29247  elmapresaunres2  29248  fzneg  29463  lsmfgcl  29565  nn01to3  30325  fzonn0p1p1  30354  ltsubsubaddltsub  30605  hashclwwlkn  30648  rusgra0edg  30711  nn0sumltlt  30880  gsumpr  30896  assa2ass  30963  lincsum  31070  trelded  31574  jaoded  31575  eel112  31726  el123  31797  suctrALT  31862  suctrALTcf  31958  bnj1384  32323  hlatjcl  33317  hlatjcom  33318  hlatlej1  33325  hlrelat5N  33351  2lplnmN  33509  2llnmj  33510  2lplnmj  33572
  Copyright terms: Public domain W3C validator