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

Theorem syl3an 1270
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 1181 . 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 973
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 975
This theorem is referenced by:  funtpg  5636  fresaun  5754  fresaunres2  5755  ftpg  6069  eloprabga  6371  cdaenun  8550  addasspi  9269  mulasspi  9271  distrpi  9272  addcanpi  9273  mulcanpi  9274  ltapi  9277  lemul1  10390  ltdiv2  10426  zletr  10903  zdivadd  10928  uztrn  11094  uzss  11098  nn01to3  11171  qdivcl  11199  maxle  11387  lemin  11388  maxlt  11389  ltmin  11390  xaddass  11437  xmulasslem3  11474  xadddilem  11482  iooneg  11636  fzen  11699  fzaddel  11714  fzrev  11738  fzrevral2  11759  fzshftral  11761  fzosubel2  11840  fzonn0p1p1  11858  fldiv2  11951  modmulnn  11976  modcyc2  11995  hashssdif  12434  ccatsymb  12559  ccatw2s1ass  12591  swrdccatin12lem1  12666  fsum0diag2  13554  efsub  13689  dvdsnegb  13855  muldvds1  13862  muldvds2  13863  dvdscmul  13864  dvdsmulc  13865  dvdscmulr  13866  dvdsmulcr  13867  dvds2add  13869  dvds2sub  13870  dvdstr  13871  divalglem8  13910  divalgb  13914  divalgmod  13916  ndvdsadd  13918  modgcd  14026  absmulgcd  14037  rpmulgcd  14045  hashdvds  14157  pythagtriplem1  14192  vdwlem3  14353  ressinbas  14544  gsumws2  15830  nmzsubg  16034  pmtr3ncomlem1  16291  pmtrdifellem1  16294  subcmn  16635  gexexlem  16648  lsmcom  16654  zaddablx  16664  assa2ass  17739  psrbagconf1o  17794  gsumbagdiaglem  17795  psrass1lem  17797  psrass1  17828  mplmonmul  17894  ply1opprmul  18048  coe1mul  18079  psgnghm  18380  2ndcdisj2  19721  fbssfi  20070  isfcf  20267  nmotri  20978  nghmplusg  20979  0nmhm  20994  iundisj2  21691  ovolioo  21710  uniiccdif  21719  basellem9  23087  nb3grapr  24126  hashclwwlkn  24509  rusgra0edg  24628  gxmodid  24954  issubgoi  24985  ablomul  25030  lnocoi  25345  ipasslem5  25423  hhssnv  25853  shscli  25908  shmodsi  25980  lnopmi  26592  lnopcoi  26595  cnlnadjlem2  26660  adjmul  26684  leopmul2i  26727  leoptr  26729  pjimai  26768  mdslle1i  26909  mdslle2i  26910  mdslj1i  26911  mdslj2i  26912  mdslmd1lem1  26917  mdslmd2i  26922  atexch  26973  atcvatlem  26977  chirredlem3  26984  sumdmdii  27007  sumdmdlem  27010  cdj3i  27033  iundisj2f  27119  iundisj2fi  27267  xrge0omnd  27360  binomrisefac  28738  cgr3permute3  29271  cgr3permute1  29272  cgr3com  29277  nndivsub  29496  mblfinlem2  29627  cnambfre  29638  ftc1anclem5  29669  fzmul  29834  fzadd2  29835  isismty  29898  heibor1  29907  heiborlem3  29910  elmapresaun  30306  elmapresaunres2  30307  fzneg  30522  lsmfgcl  30624  ltsubsubaddltsub  31793  nn0sumltlt  32003  gsumpr  32014  lincsum  32103  trelded  32418  jaoded  32419  eel112  32570  el123  32641  suctrALT  32706  suctrALTcf  32802  bnj1384  33167  hlatjcl  34163  hlatjcom  34164  hlatlej1  34171  hlrelat5N  34197  2lplnmN  34355  2llnmj  34356  2lplnmj  34418
  Copyright terms: Public domain W3C validator