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

Theorem syl3an 1226
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 1139 . 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 set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  suctr  4657  funtpg  5493  fresaun  5606  fresaunres2  5607  ftpg  5908  eloprabga  6152  cdaenun  8046  addasspi  8764  mulasspi  8766  distrpi  8767  addcanpi  8768  mulcanpi  8769  ltapi  8772  lemul1  9854  ltdiv2  9887  zdivadd  10333  uztrn  10494  uzss  10498  qdivcl  10587  maxle  10770  lemin  10771  maxlt  10772  ltmin  10773  xaddass  10820  xmulasslem3  10857  xadddilem  10865  iooneg  11009  fzen  11064  fzaddel  11079  fzrev  11100  fzrevral2  11124  fzshftral  11126  fzosubel2  11170  fldiv2  11234  modmulnn  11257  modcyc2  11269  hashssdif  11669  fsum0diag2  12558  efsub  12693  dvdsnegb  12859  muldvds1  12866  muldvds2  12867  dvdscmul  12868  dvdsmulc  12869  dvdscmulr  12870  dvdsmulcr  12871  dvds2add  12873  dvds2sub  12874  dvdstr  12875  divalglem8  12912  divalgb  12916  divalgmod  12918  ndvdsadd  12920  modgcd  13028  absmulgcd  13039  rpmulgcd  13047  hashdvds  13156  pythagtriplem1  13182  vdwlem3  13343  ressinbas  13517  gsumws2  14780  nmzsubg  14973  subcmn  15448  gexexlem  15459  lsmcom  15465  zaddablx  15475  psrbagconf1o  16431  gsumbagdiaglem  16432  psrass1lem  16434  psrass1  16461  mplmonmul  16519  ply1opprmul  16625  coe1mul  16655  2ndcdisj2  17512  fbssfi  17861  isfcf  18058  nmotri  18765  nghmplusg  18766  0nmhm  18781  iundisj2  19435  ovolioo  19454  uniiccdif  19462  basellem9  20863  nb3grapr  21454  gxmodid  21859  issubgoi  21890  ablomul  21935  lnocoi  22250  ipasslem5  22328  hhssnv  22756  shscli  22811  shmodsi  22883  lnopmi  23495  lnopcoi  23498  cnlnadjlem2  23563  adjmul  23587  leopmul2i  23630  leoptr  23632  pjimai  23671  mdslle1i  23812  mdslle2i  23813  mdslj1i  23814  mdslj2i  23815  mdslmd1lem1  23820  mdslmd2i  23825  atexch  23876  atcvatlem  23880  chirredlem3  23887  sumdmdii  23910  sumdmdlem  23913  cdj3i  23936  iundisj2f  24022  iundisj2fi  24145  binomrisefac  25350  cgr3permute3  25973  cgr3permute1  25974  cgr3com  25979  nndivsub  26199  mblfinlem  26234  cnambfre  26245  ftc1anclem5  26274  fzmul  26435  fzadd2  26436  isismty  26501  heibor1  26510  heiborlem3  26513  elmapresaun  26820  elmapresaunres2  26821  fzneg  27038  lsmfgcl  27140  psgnghm  27405  zletr  28092  ccatsymb  28152  swrdccatin12lem2  28173  trelded  28589  jaoded  28590  eel112  28742  el123  28813  suctrALTcf  28971  bnj1384  29338  hlatjcl  30101  hlatjcom  30102  hlatlej1  30109  hlrelat5N  30135  2lplnmN  30293  2llnmj  30294  2lplnmj  30356
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator