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

Theorem syl3an 1255
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 1168 . 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 960
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 962
This theorem is referenced by:  funtpg  5465  fresaun  5579  fresaunres2  5580  ftpg  5889  eloprabga  6176  cdaenun  8339  addasspi  9060  mulasspi  9062  distrpi  9063  addcanpi  9064  mulcanpi  9065  ltapi  9068  lemul1  10177  ltdiv2  10213  zletr  10685  zdivadd  10709  uztrn  10873  uzss  10877  qdivcl  10970  maxle  11158  lemin  11159  maxlt  11160  ltmin  11161  xaddass  11208  xmulasslem3  11245  xadddilem  11253  iooneg  11401  fzen  11463  fzaddel  11489  fzrev  11515  fzrevral2  11541  fzshftral  11543  fzosubel2  11596  fldiv2  11696  modmulnn  11721  modcyc2  11740  hashssdif  12163  ccatsymb  12277  ccatw2s1ass  12304  swrdccatin12lem1  12371  fsum0diag2  13246  efsub  13380  dvdsnegb  13546  muldvds1  13553  muldvds2  13554  dvdscmul  13555  dvdsmulc  13556  dvdscmulr  13557  dvdsmulcr  13558  dvds2add  13560  dvds2sub  13561  dvdstr  13562  divalglem8  13600  divalgb  13604  divalgmod  13606  ndvdsadd  13608  modgcd  13716  absmulgcd  13727  rpmulgcd  13735  hashdvds  13846  pythagtriplem1  13879  vdwlem3  14040  ressinbas  14230  gsumws2  15513  nmzsubg  15715  pmtr3ncomlem1  15972  pmtrdifellem1  15975  subcmn  16314  gexexlem  16327  lsmcom  16333  zaddablx  16343  psrbagconf1o  17422  gsumbagdiaglem  17423  psrass1lem  17425  psrass1  17456  mplmonmul  17521  ply1opprmul  17669  coe1mul  17699  psgnghm  17969  2ndcdisj2  19020  fbssfi  19369  isfcf  19566  nmotri  20277  nghmplusg  20278  0nmhm  20293  iundisj2  20989  ovolioo  21008  uniiccdif  21017  basellem9  22385  nb3grapr  23296  gxmodid  23701  issubgoi  23732  ablomul  23777  lnocoi  24092  ipasslem5  24170  hhssnv  24600  shscli  24655  shmodsi  24727  lnopmi  25339  lnopcoi  25342  cnlnadjlem2  25407  adjmul  25431  leopmul2i  25474  leoptr  25476  pjimai  25515  mdslle1i  25656  mdslle2i  25657  mdslj1i  25658  mdslj2i  25659  mdslmd1lem1  25664  mdslmd2i  25669  atexch  25720  atcvatlem  25724  chirredlem3  25731  sumdmdii  25754  sumdmdlem  25757  cdj3i  25780  iundisj2f  25867  iundisj2fi  26014  xrge0omnd  26107  binomrisefac  27474  cgr3permute3  28007  cgr3permute1  28008  cgr3com  28013  nndivsub  28233  mblfinlem2  28354  cnambfre  28365  ftc1anclem5  28396  fzmul  28561  fzadd2  28562  isismty  28625  heibor1  28634  heiborlem3  28637  elmapresaun  29034  elmapresaunres2  29035  fzneg  29250  lsmfgcl  29352  nn01to3  30112  fzonn0p1p1  30141  ltsubsubaddltsub  30392  hashclwwlkn  30435  rusgra0edg  30498  gsumpr  30675  assa2ass  30720  lincsum  30804  trelded  31107  jaoded  31108  eel112  31260  el123  31331  suctrALT  31396  suctrALTcf  31492  bnj1384  31857  hlatjcl  32733  hlatjcom  32734  hlatlej1  32741  hlrelat5N  32767  2lplnmN  32925  2llnmj  32926  2lplnmj  32988
  Copyright terms: Public domain W3C validator