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

Theorem syldan 470
Description: A syllogism deduction with conjoined antecedents. (Contributed by NM, 24-Feb-2005.) (Proof shortened by Wolf Lammen, 6-Apr-2013.)
Hypotheses
Ref Expression
syldan.1  |-  ( (
ph  /\  ps )  ->  ch )
syldan.2  |-  ( (
ph  /\  ch )  ->  th )
Assertion
Ref Expression
syldan  |-  ( (
ph  /\  ps )  ->  th )

Proof of Theorem syldan
StepHypRef Expression
1 syldan.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
2 syldan.2 . . . 4  |-  ( (
ph  /\  ch )  ->  th )
32expcom 435 . . 3  |-  ( ch 
->  ( ph  ->  th )
)
43adantrd 468 . 2  |-  ( ch 
->  ( ( ph  /\  ps )  ->  th )
)
51, 4mpcom 36 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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
This theorem is referenced by:  sylan2  474  thema2a  1591  sbcied2  3369  csbied2  3463  elpwunsn  4068  elpw2g  4610  pofun  4816  fnbr  5681  dffv2  5938  grprinvlem  6495  caofid0l  6550  caofid0r  6551  caofid1  6552  caofid2  6553  caofcom  6554  fnexALT  6747  frxp  6890  fnse  6897  brovex  6947  tfr3  7065  tz7.48-2  7104  oaf1o  7209  omlimcl  7224  oeeulem  7247  ixpexg  7490  f1domg  7532  domdifsn  7597  unxpdom2  7725  xpfir  7739  fofinf1o  7797  fofi  7802  imafi  7809  intrnfi  7872  ordtypelem6  7944  oiexg  7956  cantnfp1lem3  8095  cantnflem1  8104  cantnfp1lem3OLD  8121  cantnflem1OLD  8127  infxpenlem  8387  fseqenlem2  8402  ssnum  8416  acni2  8423  finacn  8427  fonum  8435  infpwfien  8439  inffien  8440  infunsdom1  8589  infunsdom  8590  ackbij1lem12  8607  cfslb2n  8644  fin23lem28  8716  compssiso  8750  isf34lem5  8754  fin56  8769  axcc3  8814  axdc3lem2  8827  ttukeylem6  8890  ttukeylem7  8891  brdom3  8902  gchdomtri  9003  fpwwe2lem13  9016  gchxpidm  9043  tsken  9128  tsksn  9134  tsk1  9138  tsk2  9139  2domtsk  9140  tskcard  9155  r1tskina  9156  gruss  9170  gruxp  9181  gruina  9192  grur1a  9193  ltaddpr  9408  ltexprlem7  9416  1idsr  9471  addgt0sr  9477  recexsr  9480  msqgt0  10069  mulgt1  10397  gt0div  10404  ge0div  10405  ltdiv2  10426  ltrec1  10428  lerec2  10429  lediv2  10431  lediv12a  10434  recreclt  10440  creur  10526  nn2ge  10557  avgle1  10774  recnz  10932  suprzcl  10936  uzwo2  11142  rpnnen1lem5  11208  xrrege0  11371  xlemul1a  11476  xrsupsslem  11494  xrinfmsslem  11495  supxr2  11501  supxrpnf  11506  supxrunb1  11507  supxrunb2  11508  ixxun  11541  peano2fzor  11881  ioopnfsup  11954  modcl  11963  modge0  11968  zmodcl  11978  seqcl  12090  seqf  12091  seqfveq  12094  sermono  12102  seqsplit  12103  seqcaopr2  12106  seqf1olem2  12110  seqf1o  12111  seqhomo  12117  seqz  12118  le2sq2  12205  faclbnd4lem3  12335  bcpasc  12361  hashgt0  12418  seqcoll  12472  seqcoll2  12473  hashge2el2dif  12481  wrdnval  12531  wrdsymb1  12537  ccatlid  12562  ccatass  12564  swrdtrcfvl  12632  swrdlsw  12634  2swrd1eqwrdeq  12636  ccatswrd  12638  swrd0swrd  12643  swrdccatwrd  12650  wrdeqcats1  12656  wrdeqs1cat  12657  swrdccatin2  12669  revccat  12697  revrev  12698  sqrlem7  13039  resqrex  13041  sqrtgt0  13049  leabs  13089  absmax  13118  r19.2uz  13140  lo1bdd2  13303  o1lo12  13317  rlimclim1  13324  lo1eq  13347  rlimeq  13348  rlimcn1  13367  rlimcn2  13369  rlimdiv  13424  rlimsqzlem  13427  clim2ser  13433  clim2ser2  13434  climub  13440  isercolllem1  13443  isercolllem3  13445  isercoll2  13447  climsup  13448  serf0  13459  iseraltlem1  13460  fsumf1o  13501  fsumss  13503  fsumsplit  13518  fsummsnunz  13525  fsum2dlem  13541  fsumless  13566  fsumabs  13571  telfsumo  13572  fsumparts  13576  fsumrlim  13581  fsumo1  13582  o1fsum  13583  cvgcmp  13586  cvgcmpce  13588  fsumiun  13591  binom1dif  13601  incexclem  13604  incexc  13605  isumsplit  13608  isumrpcl  13611  isumless  13613  isumsup2  13614  isumltss  13616  climcnds  13619  supcvg  13623  expcnv  13631  explecnv  13632  geomulcvg  13641  cvgrat  13648  mertenslem1  13649  efcllem  13668  ef0lem  13669  eftlub  13698  tanval3  13723  tanneg  13737  rpnnen2lem7  13808  rpnnen2lem9  13810  rpnnen2lem11  13812  ruclem9  13825  dvdssubr  13879  divalgmod  13916  bitsf1  13948  algfx  14061  eucalgcvga  14067  isprm6  14102  phimullem  14161  eulerthlem2  14164  pcid  14248  pcgcd  14253  unbenlem  14278  prmreclem4  14289  prmreclem5  14290  4sqlem9  14316  4sqlem15  14329  4sqlem16  14330  vdwlem2  14352  vdwlem6  14356  vdwlem10  14360  vdwlem11  14361  vdwlem13  14363  ramval  14378  ressabs  14546  imasaddflem  14778  imasvscaf  14787  mrcid  14861  mrcidb  14863  mrcidm  14867  fucidcl  15185  setcmon  15265  setcepi  15266  catccatid  15280  xpccatid  15308  yonedalem4c  15397  yonedainv  15401  pospo  15453  latjlej1  15545  latmlem1  15561  latledi  15569  latj32  15577  latjjdi  15583  mrelatlub  15666  mreclatBAD  15667  psss  15694  tsrlemax  15700  grpidd  15753  ismndd  15754  issubmnd  15759  subsubm  15795  gsumress  15817  gsumval2  15823  grpinvid1  15896  grpinvid2  15897  grplcan  15900  grpinvinv  15903  grpinvval2  15919  mulgass  15969  mulgpropd  15972  subginv  16000  subgmulg  16007  issubg2  16008  issubg4  16012  subsubg  16016  eqger  16043  divsinv  16052  resghm  16075  pwsdiagghm  16086  conjsubgen  16091  conjnsg  16094  subgga  16130  gass  16131  gasubg  16132  orbstafun  16141  orbsta  16143  symgextfv  16235  psgnunilem5  16312  gexcl2  16402  gexdvds3  16403  sylow1lem2  16412  sylow2blem1  16433  pj1ghm  16514  frgpup1  16586  frgpup3lem  16588  cntzspan  16640  cyggeninv  16674  lt6abl  16685  cycsubgcyg  16691  gsumval3eu  16695  gsumval3OLD  16696  gsumval3  16699  gsumzres  16702  gsumzresOLD  16706  gsumzaddlem  16722  gsumzaddlemOLD  16724  gsumzsplit  16732  gsumzsplitOLD  16733  gsum2d  16787  gsum2dOLD  16788  gsum2d2lem  16789  fsfnn0gsumfsffz  16799  dprdres  16862  dprdz  16864  dmdprdsplitlem  16871  dmdprdsplitlemOLD  16872  dprdcntz2  16873  dprddisj2  16874  dprddisj2OLD  16875  dprd2dlem1  16877  dmdprdsplit2lem  16881  dmdprdsplit2  16882  dprdsplit  16884  ablfac1c  16909  ablfac1eulem  16910  ablfac1eu  16911  pgpfac1lem2  16913  ablfac2  16927  rngidss  17009  isrngd  17017  rnglz  17019  rngrz  17020  gsumdixpOLD  17038  gsumdixp  17039  0unit  17110  unitnegcl  17111  rnginvdv  17124  invrpropd  17128  subrg1  17219  subrginv  17225  issubrg2  17229  subsubrg  17235  abvneg  17263  lmod0vs  17325  lmodvs0  17326  lmodvneg1  17333  islss3  17385  lspsnsubg  17406  lspidm  17412  lspsnneg  17432  lmhmlsp  17475  drngnidl  17656  psrass1lem  17797  psrlinv  17818  psrlidm  17824  psrlidmOLD  17825  mplsubglem  17861  mplsubglemOLD  17863  mplcoe1  17895  mplcoe5  17899  mplcoe2OLD  17901  mplind  17935  mpfind  17973  evls1val  18125  evls1rhm  18127  evl1sca  18138  xrsdsreval  18228  xrsdsreclb  18230  zringmulg  18261  zrngmulg  18267  mulgrhm  18296  mulgrhmOLD  18299  znfld  18363  cygznlem3  18372  remulg  18407  ocvlsp  18471  pjff  18507  pjf2  18509  pjfo  18510  ocvpj  18512  ishil2  18514  frlmsslsp  18593  frlmsslspOLD  18594  islinds2  18612  f1lindf  18621  mat1rngiso  18752  dmatscmcl  18769  scmatscmiddistr  18774  scmatlss  18791  scmatf  18795  scmatf1  18797  mdet0pr  18858  m2detleib  18897  mply1topmatval  19069  tgcl  19234  tgclb  19235  tgss2  19252  tgfiss  19256  opncld  19297  ntrval2  19315  ntrss3  19324  clsidm  19331  ntridm  19332  opnssneib  19379  ssnei2  19380  neindisj  19381  opnnei  19384  innei  19389  resttopon  19425  restcld  19436  restcls  19445  restntr  19446  perfopn  19449  cnpnei  19528  cncls2i  19534  cnntri  19535  cnclsi  19536  lmss  19562  pnrmopn  19607  lpcls  19628  perfcls  19629  cncmp  19655  cmpsublem  19662  cmpsub  19663  consuba  19684  clscon  19694  1stcrest  19717  lly1stc  19760  hauspwdom  19765  llycmpkgen2  19783  ptclsg  19848  txcnp  19853  txcmplem1  19874  xkococnlem  19892  qtoptopon  19937  qtopid  19938  kqopn  19967  ptunhmeo  20041  trfbas2  20076  trfbas  20077  filin  20087  filintn0  20094  trfil2  20120  fgtr  20123  trufil  20143  cfinufil  20161  elfm3  20183  fmfnfmlem4  20190  neiflim  20207  flfval  20223  flfnei  20224  fclsbas  20254  ptcmplem5  20288  cnextf  20298  cnextfres  20300  tgplacthmeo  20334  tgpconcompeqg  20342  tgpconcomp  20343  tsmssubm  20376  tsmssplit  20386  tsmsxplem1  20387  restutopopn  20473  isucn2  20514  cnextucn  20538  blpnfctr  20671  mopni2  20728  stdbdmopn  20753  met1stc  20756  metutopOLD  20817  psmetutop  20818  nrmmetd  20827  tngngp2  20898  xrsxmet  21046  metdsle  21088  climcncf  21136  icoopnst  21171  iocopnst  21172  cnheibor  21187  bndth  21190  htpyco1  21210  htpyco2  21211  phtpyco2  21222  pi1xfr  21287  pi1coghm  21293  lmmbrf  21433  lmnn  21434  caucfil  21454  cmetcaulem  21459  iscmet3  21464  cfilresi  21466  caussi  21468  causs  21469  lmle  21472  lmclimf  21474  bcthlem4  21498  bcth3  21502  rrxnm  21555  rrxcph  21556  rrxmval  21564  rrxmetlem  21566  rrxmet  21567  rrxdstprj1  21568  minveclem4  21579  ivth2  21599  ivthicc  21602  cniccbdd  21605  ovollb2  21632  ovolctb  21633  ovolunlem1a  21639  ovolunlem1  21640  ovolshftlem1  21652  ovolicc2lem1  21660  ovolicc2lem2  21661  ovolicc2lem4  21663  ovolicc2lem5  21664  uniioombllem2  21724  uniioombllem3  21726  volivth  21748  mbfss  21785  mbflimsup  21805  itg1val2  21823  i1fadd  21834  i1fmul  21835  itg1addlem4  21838  i1fmulc  21842  itg1mulc  21843  mbfi1fseqlem4  21857  itg2const2  21880  itg2seq  21881  itg2splitlem  21887  itg2split  21888  itg2addlem  21897  itg2gt0  21899  itg2cnlem2  21901  iblss  21943  iblss2  21944  itgss3  21953  itgless  21955  itgfsum  21965  itgsplit  21974  itgsplitioo  21976  itgcn  21981  ditgcl  21994  ditgswap  21995  ditgsplitlem  21996  dvconst  22052  dvaddbr  22073  dvmulbr  22074  rolle  22123  dvlip  22126  dvlipcn  22127  dvlip2  22128  dveq0  22133  dv11cn  22134  dvivthlem1  22141  dvne0  22144  lhop1lem  22146  lhop2  22148  lhop  22149  dvcnvre  22152  dvfsumle  22154  dvfsumge  22155  dvfsumabs  22156  dvfsumlem2  22160  dvfsumlem3  22161  dvfsumrlimge0  22163  dvfsumrlim  22164  ftc1lem1  22168  ftc1lem4  22172  ftc1lem5  22173  itgsubstlem  22181  deg1sclle  22245  uc1pmon1p  22284  plymullem  22345  coeeulem  22353  dgrlem  22358  dgrlb  22365  coemulhi  22382  dgrcolem2  22402  plydiveu  22425  vieta1lem2  22438  vieta1  22439  taylplem1  22489  taylplem2  22490  dvtaylp  22496  taylthlem1  22499  taylthlem2  22500  ulmdvlem1  22526  mtest  22530  radcnv0  22542  pserulm  22548  pserdvlem2  22554  abelthlem3  22559  abelthlem5  22561  abelthlem7  22564  efcvx  22575  sineq0  22644  tanord  22655  tanregt0  22656  logne0  22712  argregt0  22720  argimgt0  22722  argimlt0  22723  logneg2  22725  logcnlem3  22750  cxpsqrt  22809  loglesqrt  22857  ang180lem2  22867  isosctrlem1  22877  dcubic  22902  atanlogaddlem  22969  atanlogsub  22972  atantan  22979  atans2  22987  log2tlbnd  23001  birthdaylem2  23007  rlimcnp  23020  efrlim  23024  jensenlem1  23041  jensenlem2  23042  jensen  23043  fsumharmonic  23066  wilthlem2  23068  ftalem4  23074  ftalem5  23075  basellem3  23081  basellem4  23082  ppisval  23102  chtdif  23157  dvdsflsumcom  23189  musumsum  23193  muinv  23194  sgmmul  23201  chtleppi  23210  chtublem  23211  fsumvma  23213  chpval2  23218  chpub  23220  bposlem3  23286  lgsvalmod  23315  lgsdir2  23328  lgsdchr  23348  lgsquadlem2  23355  lgsquad2lem2  23359  chebbnd1lem1  23379  chebbnd1lem3  23381  dchrisumlem1  23399  dchrisumlem2  23400  dchrisumlem3  23401  dchrisum0fno1  23421  rpvmasum2  23422  dchrisum0lem1b  23425  dchrisum0lem1  23426  mulog2sumlem2  23445  chpdifbndlem1  23463  pntrsumbnd2  23477  pntrlog2bndlem6  23493  pntpbnd1  23496  pntlemj  23513  pntlemf  23515  qabvle  23535  padicabv  23540  padicabvcxp  23542  ostth2lem3  23545  lmiisolem  23835  ttgval  23851  colinearalg  23886  axcontlem2  23941  axcontlem7  23946  usgraedg3  24059  usgrarnedg1  24062  fargshiftfo  24311  wwlkm1edg  24408  clwlkisclwwlklem2a  24458  clwlkisclwwlk  24462  wlklenvclwlk  24512  frgrareg  24791  grpoidinvlem2  24880  grpoidinvlem3  24881  grpoideu  24884  grpoinvid1  24905  grpoinvid2  24906  grpolcan  24908  grpo2inv  24914  grpoinvop  24916  grpomuldivass  24924  grpopnpcan2  24928  grponnncan2  24929  grponpncan  24930  gxinv  24945  gxid  24948  ablo4  24962  ablomuldiv  24964  ablodivdiv4  24966  ablonnncan  24968  ablonnncan1  24970  ghgrplem1  25041  ghgrp  25043  ghablo  25044  ghsubgolem  25045  rngolz  25076  rngorz  25077  vc0  25135  vcz  25136  nvzs  25213  nvmdi  25218  nvnegneg  25219  nvsubadd  25223  nvnpcan  25228  nvmeq0  25232  nvabs  25249  nvelbl2  25273  sspmval  25319  sspz  25321  sspival  25324  sspimsval  25326  nmoub3i  25361  nmblolbii  25387  dipsubdir  25436  sspph  25443  ubthlem1  25459  minvecolem3  25465  minvecolem4  25469  htthlem  25507  hvaddsub4  25668  hi2eq  25695  shsel3  25906  pjpreeq  25989  pjeq  25990  chabs1  26107  pjspansn  26168  chscllem1  26228  chscllem2  26229  chscllem4  26231  5oalem2  26246  3oalem2  26254  pjoi0  26308  nmopub2tALT  26501  nmfnleub2  26518  eigvalcl  26553  eighmre  26555  leopmul  26726  nmopleid  26731  opsqrlem4  26735  spansncv2  26885  chcv1  26947  atcv0eq  26971  atexch  26973  chirredi  26986  cdj1i  27025  elabreximd  27079  iocinif  27257  ressmulgnn  27330  archirngz  27392  slmdvs0  27427  dvrdir  27440  rhmunitinv  27472  kerunit  27473  metider  27506  tpr2rico  27527  fsumcvg4  27565  lmdvg  27568  rezh  27585  qqhvq  27601  qtopt1  27633  logbrec  27658  indsum  27673  indpreima  27675  indf1ofs  27676  esummono  27703  esumpcvgval  27721  esumpmono  27722  esumcvg  27729  sigaclfu2  27758  cldssbrsiga  27795  eulerpartlems  27936  eulerpartlemb  27944  eulerpartlemgvv  27952  eulerpartlemgs2  27956  probun  27995  ballotlemfc0  28068  ballotlemfcc  28069  ballotlemsel1i  28088  ballotlemsima  28091  ballotlemfrceq  28104  ballotlemirc  28107  sgnneg  28116  sgnmulrp2  28119  signsply0  28145  signslema  28156  signstf0  28162  signsvfn  28176  signsvfpn  28179  signsvfnn  28180  signshf  28182  dmlogdmgm  28203  subfacp1lem4  28264  subfacp1lem5  28265  erdszelem8  28279  ptpcon  28315  cvmliftmolem1  28363  cvmliftmolem2  28364  cvmliftlem6  28372  cvmliftlem7  28373  cvmliftlem10  28376  cvmlift2lem9  28393  cvmlift2lem11  28395  cvmlift2lem12  28396  ghomgsg  28505  ghomf1olem  28506  sinccvglem  28510  lediv2aALT  28515  rtrclreclem.trans  28541  clim2prod  28596  clim2div  28597  ntrivcvgfvn0  28607  ntrivcvgmullem  28609  fprodf1o  28652  prodss  28653  fprodss  28654  fprodser  28655  fprodsplit  28669  fprodeq0  28679  fprod2dlem  28684  binomfallfaclem2  28736  dfon2lem9  28797  sltval2  28990  outsideofeq  29354  lineelsb2  29372  bpolysum  29389  bpolydiflem  29390  onsuct0  29480  fin2so  29614  mblfinlem2  29627  voliunnfl  29633  volsupnfl  29634  dvtanlem  29639  itg2gt0cn  29645  itgaddnclem2  29649  bddiblnc  29660  ftc1cnnclem  29663  ftc1cnnc  29664  ftc1anclem2  29666  ftc1anclem5  29669  ftc1anclem6  29670  ftc1anclem7  29671  ftc1anclem8  29672  ftc1anc  29673  ftc2nc  29674  areacirc  29687  opnregcld  29723  isfne  29738  lfinpfin  29773  sdclem1  29837  fdc  29839  metf1o  29849  mettrifi  29851  equivtotbnd  29875  isbnd2  29880  bndss  29883  equivbnd2  29889  ismtyima  29900  ismtybndlem  29903  heiborlem1  29908  heiborlem8  29915  ismrer1  29935  ablo4pnp  29943  ghomdiv  29947  rngoneglmul  29955  rngonegrmul  29956  rngosubdi  29957  rngosubdir  29958  isdrngo2  29962  rngohomco  29978  rngoisoco  29986  iscringd  29997  crngm4  30001  idlsubcl  30021  divrngidl  30026  unichnidl  30029  keridl  30030  maxidln1  30042  maxidln0  30043  igenidl  30061  igenidl2  30063  ispridlc  30068  dmncan1  30074  elrfirn2  30230  2rexfrabdioph  30331  3rexfrabdioph  30332  4rexfrabdioph  30333  6rexfrabdioph  30334  7rexfrabdioph  30335  elnn0rabdioph  30338  irrapxlem5  30364  pell14qrre  30395  pell14qrne0  30396  pell14qrmulcl  30401  pellfundex  30424  monotoddzzfi  30480  jm2.17c  30502  fnwe2lem2  30601  flcidc  30728  itgpowd  30787  lcmcllem  30802  lcmneg  30809  expgrowthi  30838  rfcnpre1  30972  rfcnpre2  30984  monoords  31073  fmulcl  31131  fmul01lt1lem1  31134  fmul01lt1lem2  31135  climinf  31148  itgcoscmulx  31287  itgsubsticclem  31293  itgioocnicc  31295  itgsbtaddcnst  31300  stoweidlem11  31311  stoweidlem14  31314  stoweidlem20  31320  stoweidlem26  31326  stoweidlem27  31327  stoweidlem31  31331  stoweidlem48  31348  stoweidlem51  31351  dirkercncflem2  31404  fourierdlem12  31419  fourierdlem14  31421  fourierdlem31  31438  fourierdlem41  31448  fourierdlem73  31480  fourierdlem74  31481  fourierdlem75  31482  fourierdlem76  31483  fourierdlem81  31488  fourierdlem83  31490  fourierdlem93  31500  fourierdlem97  31504  fourierdlem101  31508  fourierdlem107  31514  fourierdlem111  31518  fourierdlem112  31519  sqwvfourb  31530  pgrpgt2nabl  32024  invginvrid  32025  01eq0rng  32030  lincsumscmcl  32107  onetansqsecsq  32236  bnj594  33049  riotasv3d  33763  lssats  33809  lfl0  33862  lfladdcl  33868  lflvscl  33874  lkr0f  33891  olm11  34024  latm12  34027  cvrle  34075  cvrnle  34077  cvrne  34078  cvrval3  34209  atcvrj0  34224  atltcvr  34231  atbtwnexOLDN  34243  atbtwnex  34244  3at  34286  2atneat  34311  llncvrlpln2  34353  lplncvrlvol2  34411  dalemdnee  34462  linepsubN  34548  isline2  34570  paddasslem17  34632  pmodN  34646  pmapjlln1  34651  pclidN  34692  polval2N  34702  polssatN  34704  polpmapN  34708  2polpmapN  34709  2polvalN  34710  2polssN  34711  3polN  34712  pclss2polN  34717  2pmaplubN  34722  polatN  34727  2polatN  34728  psubclsubN  34736  pmapidclN  34738  ispsubcl2N  34743  linepsubclN  34747  polsubclN  34748  lhpoc2N  34811  ltrnlaut  34919  ltrncnv  34942  cdlemc3  34989  cdleme3b  35025  cdleme42ke  35281  trlcoat  35519  tendoid  35569  tendoex  35771  dvalveclem  35822  diaintclN  35855  diasslssN  35856  dvhgrp  35904  dvhlveclem  35905  docaclN  35921  diaocN  35922  doca2N  35923  doca3N  35924  dvadiaN  35925  djaclN  35933  djajN  35934  dibval2  35941  dibvalrel  35960  dibintclN  35964  dicvalrelN  35982  xihopellsmN  36051  dihopellsm  36052  dihsslss  36073  dih1  36083  dih1dimatlem  36126  dihlspsnat  36130  dihintcl  36141  dihmeetcl  36142  dochval2  36149  dochcl  36150  dochlss  36151  dochssv  36152  dochvalr  36154  dochvalr2  36159  dochocss  36163  dochoc  36164  dochnoncon  36188  djhcl  36197  djhlj  36198  djhexmid  36208  dvh3dim3N  36246  lcfrlem21  36360  hlhilhillem  36760
  Copyright terms: Public domain W3C validator