Theorem simplrr 762

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simplrr

Proof of Theorem simplrr

Step	Hyp	Ref	Expression
1		simpr 461	. 2
2	1	ad2antlr 726	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  pm2.61da3neOLD  2778  rmob  3430  disjxiun  4449  isotr  6232  weniso  6250  riota5f  6282  tfrlem9a  7074  oaass  7229  oeeui  7270  oaabs2  7313  resixpfo  7527  omxpenlem  7638  pw2f1olem  7641  fopwdom  7645  fofinf1o  7821  marypha1lem  7913  ordiso2  7961  oismo  7986  ixpiunwdom  8038  cantnf  8133  cantnfOLD  8155  fseqenlem1  8426  iunfictbso  8516  dfac12lem2  8545  dfac12lem3  8546  infunsdom1  8614  infpssrlem5  8708  fin23lem24  8723  isf32lem2  8755  isf32lem4  8757  isf34lem4  8778  fin1a2lem12  8812  fin1a2lem13  8813  ttukeylem6  8915  fpwwe2lem12  9040  fpwwe2lem13  9041  fpwwe2  9042  winalim2  9095  wunex2  9137  tskord  9179  prlem934  9432  mulcmpblnr  9469  dedekind  9765  addid1  9781  cnegex  9782  negeu  9833  add20  10089  divdivdiv  10270  ltmul12a  10423  lemul12a  10425  lediv12a  10463  supmul1  10533  cru  10553  uzwo3  11206  xleadd1a  11474  xmullem  11485  xmulgt0  11504  xlemul1a  11509  ixxun  11574  ixxss12  11578  ioodisj  11679  fz0fzelfz0  11809  mulexpz  12206  leexp1a  12224  expmulnbnd  12298  hashf1  12506  brfi1uzind  12532  reuccats1  12706  abs3lem  13171  rexanre  13179  cau3lem  13187  limsupgre  13304  limsupbnd2  13306  o1lo1  13360  rlimclim1  13368  rlimclim  13369  rlimcn1  13411  rlimcn2  13413  o1of2  13435  o1rlimmul  13441  lo1add  13449  lo1mul  13450  isercolllem1  13487  climcau  13493  caucvgrlem  13495  caucvgb  13502  summolem2  13538  summo  13539  modfsummod  13608  o1fsum  13627  prodmolem2  13742  isprm6  14250  isprm5  14253  rpdvds  14265  pclem  14362  pcqmul  14377  pcexp  14383  pcneg  14397  pcprmpw2  14405  pcadd  14408  pcmpt  14411  4sqlem13  14475  vdwlem2  14500  vdwlem7  14505  vdwlem12  14510  ramval  14526  ramub2  14532  ramz2  14542  ramcl  14547  cshwshashlem2  14581  imasval  14908  imasdsval  14912  mreexexd  15045  acsfn  15056  issubc3  15218  idfucl  15250  funcres2c  15270  isnat  15316  fucpropd  15346  xpcval  15446  xpcco  15452  prfval  15468  evlf2  15487  evlfcl  15491  curf12  15496  curf1cl  15497  curf2  15498  curfcl  15501  curf2ndf  15516  hof2val  15525  hofcl  15528  hofpropd  15536  yonedalem4a  15544  yonedainv  15550  drsdirfi  15567  pospo  15603  poslubmo  15776  posglbmo  15777  isipodrs  15791  acsinfd  15810  gsumvalx  15897  gsumpropd2lem  15900  ismndd  15943  mndpropd  15946  mhmeql  15995  mrcmndind  15997  frmdup3lem  16034  mhmmnd  16192  issubg4  16220  ssnmz  16243  conjnmzb  16301  f1otrspeq  16472  psgneu  16531  pgpfi  16625  sylow2blem3  16642  slwhash  16644  fislw  16645  sylow3lem2  16648  lsmdisj2  16700  pj1eu  16714  efgredlem  16765  frgpuplem  16790  gexex  16859  frgpnabl  16879  dprdfadd  17060  dprdfaddOLD  17067  dpjidcl  17107  dpjidclOLD  17114  pgpfac1lem3  17128  pgpfaclem3  17134  ablfac2  17140  ringpropd  17230  islmhm2  17684  lmhmpropd  17719  lbsextlem4  17807  assapropd  17976  psrval  18011  evlslem1  18184  prmirredlem  18523  prmirredlemOLD  18526  psgndiflemA  18637  lsmcss  18723  uvcf1  18823  frlmsslsp  18829  frlmsslspOLD  18830  frlmup1  18832  mamucl  18903  mamuass  18904  mamudi  18905  mamudir  18906  mamuvs1  18907  mamuvs2  18908  mamulid  18943  mamurid  18944  dmatsubcl  19000  dmatmulcl  19002  scmatscm  19015  marrepval  19064  marepveval  19070  mdetunilem7  19120  gsummatr01lem4  19160  cpmatmcllem  19219  mat2pmatf1  19230  mat2pmatlin  19236  decpmatmul  19273  pm2mpmhmlem2  19320  chpidmat  19348  pptbas  19509  toponmre  19594  restbas  19659  iscncl  19770  cnrest2  19787  cnpdis  19794  lmcnp  19805  dishaus  19883  cmpcovf  19891  tgcmp  19901  dfcon2  19920  clscon  19931  2ndcctbss  19956  dis2ndc  19961  1stccnp  19963  islly2  19985  cldllycmp  19996  locfincmp  20027  comppfsc  20033  kgentopon  20039  txcls  20105  ptpjopn  20113  dfac14  20119  xkoccn  20120  txcnp  20121  txcmpb  20145  txlm  20149  xkopt  20156  xkoco1cn  20158  xkoco2cn  20159  qtopcn  20215  qtoprest  20218  regr1lem2  20241  xkocnv  20315  qtophmeo  20318  fmfnfmlem4  20458  hausflim  20482  hauspwpwf1  20488  fclscmp  20531  alexsublem  20544  alexsubALTlem2  20548  alexsubALTlem3  20549  ptcmplem3  20554  ptcmplem4  20555  ptcmplem5  20556  cnextfun  20564  tmdgsum2  20595  symgtgp  20600  tsmsval2  20628  tsmsgsum  20637  tsmsgsumOLD  20640  utoptop  20737  ismet2  20836  blin  20924  metss2lem  21014  methaus  21023  met1stc  21024  met2ndci  21025  prdsxmslem2  21032  metcnp3  21043  metcnpi3  21049  metusttoOLD  21060  metustto  21061  metustfbasOLD  21068  metustfbas  21069  nlmvscn  21196  nrginvrcn  21200  xrsxmet  21314  reconnlem1  21331  reconn  21333  xrge0tsms  21339  xmetdcn2  21342  metdscn  21360  addcnlem  21368  fsumcn  21374  cnheiborlem  21454  cnheibor  21455  bndth  21458  lebnum  21464  nmoleub2lem2  21599  ipcn  21686  iscmet3  21732  caubl  21746  rrxdstprj1  21836  minveclem3b  21843  minveclem7  21850  pjthlem2  21853  pmltpc  21862  volfiniun  21957  ioombl1  21972  dyadss  22003  dyaddisjlem  22004  dyadmax  22007  dyadmbllem  22008  opnmbllem  22010  itg1addlem2  22104  itg10a  22117  mbfi1fseqlem6  22127  itg2seq  22149  itg2monolem1  22157  itg2gt0  22167  itgfsum  22233  limcfval  22276  ellimc2  22281  ellimc3  22283  limcres  22290  limciun  22298  dvres  22315  dveflem  22380  rolle  22391  dvlip2  22396  c1liplem1  22397  dvgt0lem1  22403  dvgt0  22405  dvlt0  22406  dvne0  22412  dvfsumrlimge0  22431  ftc1lem6  22442  itgsubst  22450  mdegmullem  22478  ply1domn  22524  ply1divex  22537  fta1g  22568  fta1b  22570  plyf  22595  dgrlem  22626  coeid  22635  plydivalg  22695  aannenlem1  22724  aalioulem3  22730  aalioulem6  22733  abelthlem8  22834  efif1olem4  22932  chordthm  23168  xrlimcnp  23298  jensen  23318  sqf11  23413  fsumvma2  23489  perfectlem2  23505  lgsdilem  23597  lgsquad2lem2  23634  lgsquad3  23636  2sqlem5  23643  2sqlem9  23648  2sqb  23653  rpvmasumlem  23672  dchrisum0flb  23695  dchrisum0  23705  pntpbnd  23773  pntibndlem3  23777  pntleml  23796  legov  23972  legtrid  23978  tglinethru  24016  tglnpt2  24021  tglineintmo  24022  mirreu3  24035  perpcom  24090  colperpexlem3  24106  mideu  24112  opphllem1  24119  lnopp2hpgb  24132  brcgr  24203  brbtwn2  24208  colinearalg  24213  axsegcon  24230  axeuclidlem  24265  axcontlem9  24275  ecgrtg  24286  elntg  24287  eengtrkg  24288  cusgrarn  24459  usgrasscusgra  24483  4cycl4dv4e  24668  wwlkext2clwwlk  24803  usg2spthonot1  24890  usgfidegfi  24910  eupath2  24980  usg2spot2nb  25065  numclwwlk6  25113  vacn  25604  blocni  25720  ubthlem3  25788  minvecolem7  25799  chocunii  26219  pjhthmo  26220  pjhthlem2  26310  kbass5  27039  mdsymlem5  27326  foresf1o  27403  fcobij  27548  xrofsup  27582  archirngz  27733  archiabllem2a  27738  xrge0tsmsd  27775  isarchiofld  27807  reff  27842  ordtconlem1  27906  qqhval2  27963  volmeas  28203  ballotlemfc0  28431  ballotlemfcc  28432  signstfvneq0  28529  lgamcvglem  28582  lgamcvg2  28597  derangenlem  28615  erdsze2lem1  28647  pconcon  28676  conpcon  28680  cvxscon  28688  cvmliftmolem2  28727  cvmliftmo  28729  cvmlift2lem10  28757  cvmlift2lem12  28759  cvmlift3lem7  28770  mrsubff1  28874  msubff1  28916  poseq  29333  ifscgr  29694  cgrxfr  29705  btwnconn1lem13  29749  btwnconn1lem14  29750  outsideofeq  29780  ellines  29802  supaddc  30041  opnmbllem0  30050  mblfinlem3  30053  itg2addnclem  30066  itg2addnc  30069  ftc1cnnc  30089  finminlem  30136  fnejoin2  30187  upixp  30220  filbcmb  30231  sstotbnd2  30270  isbnd3  30280  prdsbnd2  30291  cntotbnd  30292  ismtyima  30299  bfp  30320  rrncmslem  30328  unichnidl  30428  nacsfix  30644  mzpsubst  30681  mzpcompact2lem  30684  eldioph2lem2  30694  eldioph2  30695  eldioph2b  30696  diophin  30706  diophun  30707  irrapxlem3  30760  irrapxlem5  30762  pell1234qrreccl  30790  pell1234qrmulcl  30791  pell14qrdich  30805  pell1qrge1  30806  pell1qrgaplem  30809  monotuz  30877  rpexpmord  30884  acongtr  30916  acongrep  30918  jm2.23  30938  jm2.26a  30942  jm2.26lem3  30943  jm2.26  30944  jm2.27  30950  wepwsolem  30987  fnwe2lem2  30997  kelac1  31009  kercvrlsm  31029  hbtlem5  31077  hbt  31079  mpaaeu  31099  cncmpmax  31407  rfcnnnub  31411  iccintsng  31563  lptioo2  31637  lptioo1  31638  limclner  31657  stoweidlem31  31813  stoweidlem34  31816  stoweidlem35  31817  stoweidlem49  31831  stoweidlem59  31841  stoweidlem62  31844  fourierdlem60  31949  fourierdlem61  31950  fourierdlem87  31976  usgedgvadf1lem2  32414  usgedgvadf1ALTlem2  32417  mgmhmeql  32491  mndpsuppss  32964  scmsuppss  32965  lindslinindsimp2lem5  33063  lshpcmp  34713  islshpat  34742  lfl0f  34794  ishlat3N  35079  3dim1  35191  islvol5  35303  lvoli2  35305  lncvrelatN  35505  pclfinclN  35674  pexmidlem8N  35701  idltrn  35874  cdleme42keg  36212  cdleme42mgN  36214  cdlemf2  36288  cdlemg2cex  36317  trlcoat  36449  dihopelvalcpre  36975  dih1dimatlem  37056  dihjatcclem4  37148  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