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

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

Proof of Theorem simprrl
StepHypRef Expression
1 simpl 457 . 2
21ad2antll 728 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  grpridd  6515  eroveu  7425  undom  7625  mapdom2  7708  domunfican  7813  fofinf1o  7821  finsschain  7847  wemaplem3  7994  oemapvali  8124  iunfictbso  8516  enfin2i  8722  fin1a2s  8815  ttukeylem6  8915  distrlem4pr  9425  mulcmpblnr  9469  prsrlem1  9470  dedekind  9765  divdivdiv  10270  divmuleq  10274  divsubdiv  10285  lediv12a  10463  xralrple  11433  ssfzo12bi  11907  seqcaopr  12144  leexp2r  12223  hashbclem  12501  wrd2ind  12703  rlimresb  13388  summo  13539  fsum2dlem  13585  prodmo  13743  fprod2dlem  13784  bezoutlem3  14178  bezoutlem4  14179  qredeu  14248  pcqmul  14377  pcadd  14408  pockthg  14424  prmreclem2  14435  vdwlem10  14508  ramub1lem2  14545  cshwsdisj  14583  mreexexlem4d  15044  mreexdomd  15046  issubc3  15218  cofucl  15257  setcmon  15414  setcepi  15415  drsdirfi  15567  poslubmo  15776  posglbmo  15777  issubmd  15980  mrcmndind  15997  ghmpreima  16288  gaorber  16346  psgnunilem4  16522  psgneu  16531  odcau  16624  pgpssslw  16634  fislw  16645  lsmsubm  16673  efgsfo  16757  gsum2d2  17002  pgpfac1lem5  17130  pgpfac1  17131  pgpfaclem2  17133  pgpfaclem3  17134  unitgrp  17316  lmodprop2d  17572  lsspropd  17663  lbsextlem4  17807  assapropd  17976  evlslem1  18184  mdetunilem8  19121  mdetuni0  19123  mdetmul  19125  neiint  19605  restbas  19659  iscnp4  19764  cnpco  19768  nrmsep  19858  regsep2  19877  ordthauslem  19884  1stcfb  19946  1stcrest  19954  2ndcctbss  19956  2ndcdisj  19957  2ndcomap  19959  dis2ndc  19961  nlly2i  19977  islly2  19985  hausllycmp  19995  lly1stc  19997  comppfsc  20033  ptbasin  20078  txcls  20105  ptcnp  20123  txlly  20137  txnlly  20138  txtube  20141  txcmplem1  20142  txcmplem2  20143  xkococnlem  20160  basqtop  20212  regr1lem  20240  kqreglem1  20242  kqreglem2  20243  kqnrmlem1  20244  kqnrmlem2  20245  reghmph  20294  nrmhmph  20295  opnfbas  20343  rnelfmlem  20453  fmufil  20460  fclscf  20526  fclsfnflim  20528  flimfnfcls  20529  uffclsflim  20532  cnpfcfi  20541  cnpfcf  20542  alexsubALTlem2  20548  alexsubALTlem4  20550  tgpconcompeqg  20610  ghmcnp  20613  qustgplem  20619  tsmsxp  20657  blssps  20927  blss  20928  blcld  21008  metequiv2  21013  met2ndci  21025  prdsxmslem2  21032  txmetcnp  21050  nlmvscnlem1  21195  xrge0tsms  21339  ipcnlem1  21685  iscmet3  21732  cmetss  21753  minveclem3  21844  pmltpc  21862  ovolscalem2  21925  ovolicc2lem5  21932  ovolicc2  21933  nulmbl2  21947  ioombl1  21972  uniioombllem6  21997  uniioombl  21998  vitalilem3  22019  i1faddlem  22100  mbfmullem  22132  itg2split  22156  lhop2  22416  dvfsumrlim  22432  itgsubst  22450  plydivex  22693  plyexmo  22709  ulmbdd  22793  cxploglim  23307  dchrptlem2  23540  lgsquad2lem2  23634  2sqlem5  23643  dchrvmasumif  23688  rpvmasum2  23697  dchrisum0re  23698  dchrisum0lem3  23704  dchrisum0  23705  dchrmusum  23709  dchrvmasum  23710  pntibndlem3  23777  pntlemp  23795  ostth3  23823  legtrid  23978  mirreu3  24035  midexlem  24069  opphllem  24109  mideulem  24110  opphllem1  24119  ax5seglem9  24240  ax5seg  24241  axcontlem8  24274  axcontlem12  24278  cusgrafilem1  24479  2spotiundisj  25062  ablo4  25289  smcnlem  25607  pjhthmo  26220  mdslmd1lem1  27244  xrge0tsmsd  27775  locfinref  27844  xpinpreima2  27889  qqhval2  27963  dya2iocnrect  28252  orvcgteel  28406  orvclteel  28411  derangenlem  28615  cnpcon  28675  txpcon  28677  conpcon  28680  pconpi1  28682  iccllyscon  28695  rellyscon  28696  cvmcov2  28720  cvmliftmolem2  28727  cvmliftmo  28729  cvmliftlem15  28743  cvmliftpht  28763  cvmlift3lem2  28765  relexpsucl  29055  relexpcnv  29056  relexpdm  29058  relexprn  29059  relexpadd  29061  relexpindlem  29062  rtrclreclem.trans  29069  rtrclreclem.min  29070  rtrclind  29072  cgrextend  29658  btwnouttr2  29672  cgrsub  29695  cgrxfr  29705  btwnxfr  29706  colineardim1  29711  btwnconn1lem6  29742  btwnconn1lem13  29749  btwnconn1lem14  29750  btwnconn3  29753  seglecgr12im  29760  segleantisym  29765  outsideofeq  29780  outsidele  29782  lineunray  29797  linethru  29803  mblfinlem3  30053  cnambfre  30063  areacirclem5  30111  fnessref  30175  neibastop2lem  30178  neibastop2  30179  istotbnd3  30267  sstotbnd  30271  crngm4  30400  diophin  30706  pellexlem3  30767  pellexlem5  30769  pellex  30771  pell14qrmulcl  30799  jm2.19lem3  30933  jm2.25  30941  jm2.27b  30948  lmhmfgsplit  31032  hbtlem2  31073  hbtlem5  31077  fnchoice  31404  stoweidlem17  31799  stoweidlem53  31835  stoweidlem61  31843  rabsubmgmd  32479  lindslinindsimp1  33058  bj-finsumval0  34663  cvlcvr1  35064  4atlem12  35336  paddasslem10  35553  paddasslem12  35555  paddasslem13  35556  lhpexle3lem  35735  cdlemd4  35926  cdleme0cq  35940  cdlemefs32sn1aw  36140  cdleme43fsv1snlem  36146  cdleme32d  36170  cdleme32f  36172  cdleme40m  36193  cdleme40n  36194  cdleme42keg  36212  cdleme42mgN  36214  cdleme50trn2  36277  cdleme50trn3  36279  cdlemm10N  36845  dihvalcqpre  36962  dihopelvalcpre  36975  dihmeetlem1N  37017  dihjat1lem  37155  mapd0  37392  mapdh9a  37517
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