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  5450  fresaunres2  5451  eloprabga  5976  cdaenun  7845  addasspi  8564  mulasspi  8566  distrpi  8567  addcanpi  8568  mulcanpi  8569  ltapi  8572  lemul1  9653  ltdiv2  9686  zdivadd  10130  uztrn  10291  uzss  10295  qdivcl  10384  maxle  10566  lemin  10567  maxlt  10568  ltmin  10569  xaddass  10616  xmulasslem3  10653  xadddilem  10661  iooneg  10803  fzen  10858  fzaddel  10873  fzrev  10893  fzrevral2  10914  fzshftral  10916  fzosubel2  10956  fldiv2  11012  modmulnn  11035  modcyc2  11047  hashssdif  11421  fsum0diag2  12292  efsub  12427  dvdsnegb  12593  muldvds1  12600  muldvds2  12601  dvdscmul  12602  dvdsmulc  12603  dvdscmulr  12604  dvdsmulcr  12605  dvds2add  12607  dvds2sub  12608  dvdstr  12609  divalglem8  12646  divalgb  12650  divalgmod  12652  ndvdsadd  12654  modgcd  12762  absmulgcd  12773  rpmulgcd  12781  hashdvds  12890  pythagtriplem1  12916  vdwlem3  13077  ressinbas  13251  gsumws2  14514  nmzsubg  14707  subcmn  15182  gexexlem  15193  lsmcom  15199  zaddablx  15209  psrbagconf1o  16169  gsumbagdiaglem  16170  psrass1lem  16172  psrass1  16199  mplmonmul  16257  ply1opprmul  16366  coe1mul  16396  2ndcdisj2  17239  fbssfi  17584  isfcf  17781  nmotri  18300  nghmplusg  18301  0nmhm  18316  iundisj2  18959  ovolioo  18978  uniiccdif  18986  basellem9  20379  gxmodid  20999  issubgoi  21030  ablomul  21075  lnocoi  21390  ipasslem5  21468  hhssnv  21896  shscli  21951  shmodsi  22023  lnopmi  22635  lnopcoi  22638  cnlnadjlem2  22703  adjmul  22727  leopmul2i  22770  leoptr  22772  pjimai  22811  mdslle1i  22952  mdslle2i  22953  mdslj1i  22954  mdslj2i  22955  mdslmd1lem1  22960  mdslmd2i  22965  atexch  23016  atcvatlem  23020  chirredlem3  23027  sumdmdii  23050  sumdmdlem  23053  cdj3i  23076  iundisj2f  23172  iundisj2fi  23302  cgr3permute3  25056  cgr3permute1  25057  cgr3com  25062  nndivsub  25282  fzmul  25592  fzadd2  25593  lpss2  25617  isismty  25673  heibor1  25682  heiborlem3  25685  elmapresaun  25998  elmapresaunres2  25999  fzneg  26217  lsmfgcl  26320  psgnghm  26585  funtpg  27232  ftpg  27234  nb3grapr  27399  trelded  27825  jaoded  27826  eel112  27977  el123  28048  suctrALTcf  28209  suctrALT4  28215  bnj1384  28573  hlatjcl  29374  hlatjcom  29375  hlatlej1  29382  hlrelat5N  29408  2lplnmN  29566  2llnmj  29567  2lplnmj  29629
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