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

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

Proof of Theorem simplrl
StepHypRef Expression
1 simpl 457 . 2
21ad2antlr 726 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  pm2.61da3neOLD  2778  rmob  3430  disjxiun  4449  f1imass  6172  soisoi  6224  riota5f  6282  tfrlem9a  7074  oeeui  7270  oaabs2  7313  omabs  7315  omxpenlem  7638  fopwdom  7645  frfi  7785  marypha1lem  7913  ordiso2  7961  oismo  7986  wemaplem3  7994  cantnf  8133  cantnfOLD  8155  isinffi  8394  dfac12lem2  8545  dfac12lem3  8546  infxp  8616  infmap2  8619  infpssrlem5  8708  fin23lem11  8718  fin23lem24  8723  fin23lem26  8726  isf32lem2  8755  isf32lem4  8757  fin1a2lem13  8813  fin1a2s  8815  ttukeylem5  8914  fpwwe2lem12  9040  fpwwe2lem13  9041  wunex2  9137  tskord  9179  prlem934  9432  mulcmpblnr  9469  dedekind  9765  addid1  9781  cnegex  9782  negeu  9833  add20  10089  divdivdiv  10270  ltmul12a  10423  lediv12a  10463  cru  10553  uzwo3  11206  xleadd1a  11474  xlemul1a  11509  ixxun  11574  ixxss12  11578  elfz0ubfz0  11807  mulexpz  12206  leexp1a  12224  expmulnbnd  12298  swrdccat3  12717  abs3lem  13171  rexanre  13179  cau3lem  13187  lo1bdd2  13347  o1lo1  13360  rlimclim1  13368  rlimclim  13369  lo1resb  13387  o1resb  13389  rlimcn2  13413  o1of2  13435  o1rlimmul  13441  lo1add  13449  lo1mul  13450  isercolllem1  13487  climcau  13493  summolem2  13538  summo  13539  o1fsum  13627  prodmolem2  13742  qredeu  14248  isprm5  14253  pclem  14362  pcqmul  14377  pcexp  14383  pcneg  14397  pcprmpw2  14405  pcadd  14408  prmpwdvds  14422  4sqlem13  14475  vdwlem2  14500  vdwlem7  14505  vdwlem11  14509  vdwlem12  14510  ramval  14526  ramz2  14542  ramcl  14547  cshwshashlem2  14581  imasval  14908  imasdsval  14912  mreexexd  15045  issubc3  15218  idfucl  15250  funcres2c  15270  fucpropd  15346  xpcval  15446  prfval  15468  evlfcl  15491  curf12  15496  curf1cl  15497  curf2  15498  curfcl  15501  curfuncf  15507  curf2ndf  15516  hof2val  15525  hofcl  15528  hofpropd  15536  yonedalem4a  15544  yonedainv  15550  poslubmo  15776  posglbmo  15777  isipodrs  15791  acsmapd  15808  acsinfd  15810  ismndd  15943  mndpropd  15946  mhmeql  15995  mrcmndind  15997  frmdup3lem  16034  mhmmnd  16192  issubg4  16220  ssnmz  16243  f1otrspeq  16472  psgneu  16531  sylow2blem3  16642  lsmdisj2  16700  pj1eu  16714  efgredlem  16765  frgpuplem  16790  frgpnabl  16879  dmdprdsplitlem  17084  dmdprdsplitlemOLD  17085  pgpfac1lem3  17128  pgpfaclem3  17134  ringpropd  17230  dvdsrtr  17301  islmhm2  17684  lmhmpropd  17719  assapropd  17976  evlslem1  18184  coe1tmmul2  18317  prmirredlem  18523  prmirredlemOLD  18526  psgndiflemA  18637  lsmcss  18723  dsmmlss  18775  uvcf1  18823  frlmup1  18832  mamucl  18903  mamuass  18904  mamudi  18905  mamudir  18906  mamuvs1  18907  mamuvs2  18908  mamulid  18943  mamurid  18944  dmatsubcl  19000  dmatmulcl  19002  mdetunilem7  19120  mdetunilem9  19122  cramer0  19192  cpmatmcllem  19219  mat2pmatf1  19230  decpmatmul  19273  pmatcollpw1  19277  pm2mpf1lem  19295  pm2mpmhmlem2  19320  chpidmat  19348  cpmadugsumlemB  19375  cpmadugsumlemC  19376  toponmre  19594  restbas  19659  iscncl  19770  cnpdis  19794  lmcnp  19805  dishaus  19883  cmpcovf  19891  hauscmplem  19906  dfcon2  19920  clscon  19931  2ndcctbss  19956  1stccnp  19963  islly2  19985  llyidm  19989  cldllycmp  19996  locfincmp  20027  kgentopon  20039  1stckgenlem  20054  ptpjpre1  20072  ptbasfi  20082  txcls  20105  ptpjopn  20113  xkoccn  20120  txcnp  20121  txcmpb  20145  xkoptsub  20155  xkoco2cn  20159  xkoinjcn  20188  qtopcn  20215  qtoprest  20218  regr1lem  20240  regr1lem2  20241  kqreglem1  20242  qtophmeo  20318  fgabs  20380  hauspwpwf1  20488  flimfnfcls  20529  fclscmp  20531  cnpfcf  20542  ptcmplem4  20555  ptcmplem5  20556  cnextfval  20562  cnextfun  20564  tmdgsum2  20595  tsmsval2  20628  utoptop  20737  utop3cls  20754  ismet2  20836  blin  20924  metss2lem  21014  methaus  21023  met1stc  21024  met2ndci  21025  metcnp  21044  metcnpi3  21049  metusttoOLD  21060  metustto  21061  metustfbasOLD  21068  metustfbas  21069  nlmvscn  21196  nrginvrcn  21200  nghmcn  21252  xrsxmet  21314  reconnlem1  21331  reconn  21333  xrge0tsms  21339  xmetdcn2  21342  metdscn  21360  addcnlem  21368  mulc1cncf  21409  cncfco  21411  cnheiborlem  21454  cnheibor  21455  nmoleub2lem2  21599  ipcn  21686  iscfil3  21712  cfilfcls  21713  iscmet3  21732  caubl  21746  bcthlem5  21767  rrxdstprj1  21836  minveclem3b  21843  minveclem7  21850  pmltpc  21862  ovolshftlem1  21920  ovolscalem1  21924  ioombl1  21972  uniioombllem6  21997  dyadss  22003  dyaddisjlem  22004  dyadmax  22007  opnmbllem  22010  itg1addlem2  22104  itg2seq  22149  bddmulibl  22245  limcfval  22276  ellimc3  22283  limciun  22298  dveflem  22380  rolle  22391  dvlip2  22396  c1liplem1  22397  dvgt0lem1  22403  dvgt0  22405  dvlt0  22406  dvne0  22412  dvcnvre  22420  dvfsumrlimge0  22431  ftc1lem6  22442  itgsubst  22450  mdegmullem  22478  ply1domn  22524  fta1g  22568  fta1b  22570  dgrlem  22626  coeid  22635  plydivalg  22695  aannenlem1  22724  aalioulem6  22733  ulmcn  22794  mtestbdd  22800  abelthlem8  22834  efif1olem4  22932  chordthm  23168  xrlimcnp  23298  isppw2  23389  fsumvma2  23489  perfectlem2  23505  lgsdilem  23597  lgsquad2lem2  23634  lgsquad3  23636  2sqlem5  23643  2sqlem9  23648  rpvmasumlem  23672  dchrisum0flb  23695  pntpbnd  23773  pntibndlem3  23777  pntlem3  23794  pntleml  23796  tgbtwnconn1lem3  23961  legtrid  23978  tglinethru  24016  tglnpt2  24021  tglineintmo  24022  mirreu3  24035  perpcom  24090  footex  24095  mideu  24112  opphllem1  24119  lnopp2hpgb  24132  axsegcon  24230  axpasch  24244  axeuclidlem  24265  ecgrtg  24286  elntg  24287  eengtrkg  24288  usgrasscusgra  24483  4cycl4dv4e  24668  wwlknext  24724  clwwisshclwwlem  24806  usg2spthonot1  24890  eupath2  24980  usg2spot2nb  25065  numclwlk1lem2foa  25091  numclwwlk6  25113  vacn  25604  ubthlem1  25786  ubthlem3  25788  minvecolem7  25799  chocunii  26219  pjhthmo  26220  pjhthlem2  26310  nmopub2tALT  26828  nmfnleub2  26845  kbass5  27039  mdslmd1lem1  27244  mdslmd1lem2  27245  mdsymlem5  27326  fcobij  27548  xrofsup  27582  archiabllem2a  27738  gsumvsca1  27773  gsumvsca2  27774  xrge0tsmsd  27775  isarchiofld  27807  reff  27842  ordtconlem1  27906  qqhval2  27963  esumpcvgval  28084  imambfm  28233  ballotlemsf1o  28452  signstfvneq0  28529  lgamgulmlem5  28575  pconcon  28676  conpcon  28680  cvmliftmo  28729  cvmlift2lem10  28757  cvmlift2lem12  28759  cvmlift3lem7  28770  mrsubff1  28874  msubff1  28916  ifscgr  29694  cgrxfr  29705  btwnconn1lem13  29749  ellines  29802  heicant  30049  opnmbllem0  30050  mblfinlem3  30053  itg2addnclem  30066  itg2addnc  30069  ftc1cnnc  30089  sstotbnd  30271  cntotbnd  30292  ismtyima  30299  heibor1lem  30305  heiborlem10  30316  bfp  30320  rrncmslem  30328  isnacs3  30642  nacsfix  30644  mzpsubst  30681  eldioph2lem2  30694  eldioph2  30695  eldioph2b  30696  diophin  30706  diophun  30707  rencldnfilem  30754  irrapxlem3  30760  irrapxlem5  30762  pell1234qrreccl  30790  pell1234qrmulcl  30791  pell1qrge1  30806  pell1qrgaplem  30809  monotuz  30877  monotoddzzfi  30878  rpexpmord  30884  acongtr  30916  acongrep  30918  jm2.26a  30942  jm2.26lem3  30943  jm2.26  30944  jm2.27b  30948  jm2.27  30950  wepwsolem  30987  fnwe2lem2  30997  hbtlem5  31077  hbt  31079  mpaaeu  31099  fnchoice  31404  rfcnnnub  31411  ioondisj2  31525  iccintsng  31563  lptioo2  31637  lptioo1  31638  limclner  31657  dvdsn1add  31736  stoweidlem14  31796  stoweidlem27  31809  stoweidlem34  31816  stoweidlem49  31831  stoweidlem56  31838  fourierdlem87  31976  usgedgvadf1lem2  32414  usgedgvadf1ALTlem2  32417  mgmhmeql  32491  rngcinv  32789  rngcinvOLD  32801  ringcinv  32840  ringcinvOLD  32864  mndpsuppss  32964  lindslinindsimp2lem5  33063  islshpsm  34705  lsatcmp  34728  islshpat  34742  lfl0f  34794  iscvlat2N  35049  ishlat3N  35079  3dim1  35191  islvol5  35303  lvoli2  35305  lncvrelatN  35505  lncmp  35507  paddasslem10  35553  pclfinclN  35674  pexmidlem8N  35701  idltrn  35874  cdleme42keg  36212  cdleme42mgN  36214  cdlemf2  36288  cdlemg2cex  36317  trlcoat  36449  tendoex  36701  erngdvlem4  36717  erngdvlem4-rN  36725  dialss  36773  dibglbN  36893  diblss  36897  dihlsscpre  36961  dihglblem2aN  37020  dihglblem4  37024  dihglblem5  37025  dih1dimatlem  37056  dihglblem6  37067  lcfl7N  37228  lcfrlem9  37277  mapdh9a  37517  hdmapglem7  37659
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