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

Theorem simprlr 764
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simprlr

Proof of Theorem simprlr
StepHypRef Expression
1 simpr 461 . 2
21ad2antrl 727 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  disjxiun  4449  fcof1  6190  fliftfun  6210  domunfican  7813  finsschain  7847  suppeqfsuppbi  7863  fsuppunbi  7870  wemapsolem  7996  wemapso  7997  wemapso2OLD  7998  wemapso2lem  7999  cantnf  8133  cantnfOLD  8155  enfin2i  8722  ttukeylem7  8916  fpwwe2lem2  9031  fpwwe2lem9  9037  fpwwe2lem12  9040  fpwwelem  9044  distrlem4pr  9425  mulcmpblnr  9469  prsrlem1  9470  addsrmo  9471  mulsrmo  9472  divdivdiv  10270  divsubdiv  10285  lediv12a  10463  xmullem  11485  xlemul1a  11509  seqcaopr  12144  leexp2r  12223  hashf1lem1  12504  hashf1lem2  12505  brfi1uzind  12532  wrd2ind  12703  cshweqrep  12789  summolem2  13538  summo  13539  prodmolem2  13742  prodmo  13743  bezoutlem3  14178  bezoutlem4  14179  qredeu  14248  pcadd  14408  vdwlem9  14507  vdwlem10  14508  ramub1lem2  14545  ramub1  14546  cofucl  15257  setcmon  15414  poslubmo  15776  posglbmo  15777  grprcan  16083  isnsg3  16235  ghmpreima  16288  gaorber  16346  psgneu  16531  odcau  16624  lsmsubm  16673  lsmmod  16693  efgsfo  16757  ablfaclem3  17138  ringpropd  17230  islmodd  17518  lmodprop2d  17572  lss1d  17609  assamulgscmlem2  17998  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  evlslem1  18184  lindff1  18855  islindf4  18873  mdetunilem7  19120  mdetunilem8  19121  mdetunilem9  19122  mdetuni0  19123  mdetmul  19125  ppttop  19508  epttop  19510  cnhaus  19855  isreg2  19878  cncmp  19892  1stcfb  19946  2ndcomap  19959  cldllycmp  19996  txcls  20105  ptclsg  20116  ptcnp  20123  txdis1cn  20136  txlly  20137  txnlly  20138  pthaus  20139  txhaus  20148  txkgen  20153  xkohaus  20154  xkococnlem  20160  xkococn  20161  fgabs  20380  rnelfm  20454  hausflimi  20481  hausflim  20482  alexsubALTlem2  20548  alexsubALTlem4  20550  alexsubALT  20551  tgpconcomp  20611  qustgplem  20619  metequiv2  21013  met2ndci  21025  nrmmetd  21095  nlmvscnlem1  21195  reconn  21333  xrge0tsms  21339  ipcnlem1  21685  minveclem3  21844  pmltpc  21862  ovolicc2lem5  21932  ovolicc2  21933  uniioombllem6  21997  dyadmbllem  22008  vitalilem3  22019  mbfmullem  22132  itg2split  22156  itg2mono  22160  dvlip2  22396  lhop1  22415  dvcnvrelem1  22418  ftc1lem6  22442  itgsubst  22450  dgrco  22672  plyexmo  22709  ulmdvlem3  22797  abelthlem2  22827  abelthlem8  22834  dvdsmulf1o  23470  chpchtsum  23494  dchrptlem2  23540  2sqlem5  23643  2sqlem9  23648  2sqb  23653  pntrlog2bnd  23769  pntibndlem3  23777  pntlemp  23795  pnt3  23797  mirreu3  24035  axsegcon  24230  ax5seglem9  24240  axeuclid  24266  axcontlem12  24278  clwwlkf1  24796  wwlkext2clwwlk  24803  frgranbnb  25020  ablo4  25289  ghgrpOLD  25370  smcnlem  25607  pjhthmo  26220  pjpjpre  26337  3oalem2  26581  lnconi  26952  atom1d  27272  resf1o  27553  xrge0tsmsd  27775  ballotlemfc0  28431  ballotlemfcc  28432  pconcon  28676  cvmfolem  28724  cvmliftmo  28729  cvmliftlem7  28736  cvmlift2lem10  28757  cvmlift3lem8  28771  lineext  29726  linecgr  29731  btwnconn1lem10  29746  btwnconn1lem11  29747  btwnconn3  29753  brsegle  29758  seglecgr12im  29760  segleantisym  29765  outsideoftr  29779  outsideofeq  29780  outsideofeu  29781  linethru  29803  mblfinlem3  30053  bddiblnc  30085  ftc1cnnc  30089  finminlem  30136  neibastop2lem  30178  isbnd3  30280  heibor1lem  30305  crngm4  30400  mzpcl2  30662  mzpmfp  30679  mzpmfpOLD  30680  mzpcompact2lem  30684  diophin  30706  pell14qrmulcl  30799  hbtlem2  31073  stoweidlem61  31843  fourierdlem92  31981  snlindsntor  33072  cvlcvr1  35064  4atlem12  35336  paddasslem12  35555  paddasslem13  35556  lhpexle2lem  35733  trlord  36295  cdlemkid4  36660  dihopelvalcpre  36975  dihmeetlem1N  37017  dihglblem5apreN  37018  dihmeetlem6  37036  dih1dimatlem0  37055  dihjatcclem4  37148
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
  Copyright terms: Public domain W3C validator