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

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

Proof of Theorem simpllr
StepHypRef Expression
1 simpr 461 . 2
21ad2antrr 725 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  simp-4r  768  soisoi  6224  f1o2ndf1  6908  tz7.49  7129  omabs  7315  omxpenlem  7638  fopwdom  7645  findcard3  7783  frfi  7785  finsschain  7847  marypha1lem  7913  wdomtr  8022  cantnfp1  8121  cantnfp1OLD  8147  harcard  8380  numacn  8451  infunsdom1  8614  cofsmo  8670  sornom  8678  ssfin4  8711  fin1a2lem11  8811  fin1a2lem13  8813  ttukeylem5  8914  fpwwe2lem13  9041  pwfseq  9063  mulcmpblnr  9469  00id  9776  addid1  9781  cnegex  9782  negeu  9833  add20  10089  ltmul12a  10423  lediv12a  10463  cru  10553  qextltlem  11430  xleadd1a  11474  xmullem  11485  xlemul1a  11509  ixxss12  11578  ioodisj  11679  fsuppmapnn0fz  12102  seqf1o  12148  mulexpz  12206  leexp1a  12224  faclbnd  12368  swrdswrdlem  12684  abs3lem  13171  cau3lem  13187  rlim3  13321  ello12  13339  lo1bdd2  13347  elo12  13350  rlimconst  13367  isercoll  13490  climcau  13493  climbdd  13494  summolem2  13538  fsumconst  13605  o1fsum  13627  incexclem  13648  fprodconst  13782  bitsfzo  14085  dvdsmulgcd  14192  pc2dvds  14402  pcz  14404  pcadd  14408  pcfac  14418  vdwmc2  14497  vdwlem2  14500  vdwlem10  14508  vdw  14512  ramcl  14547  sbcie3s  14676  firest  14830  prdsval  14852  mreexd  15039  mreexexlemd  15041  iscat  15069  cidfval  15073  iscatd2  15078  catcocl  15082  catass  15083  catpropd  15104  cidpropd  15105  moni  15131  monpropd  15132  issubc  15204  subccocl  15214  funcco  15240  funcpropd  15269  fullpropd  15289  nati  15324  natpropd  15345  fucpropd  15346  xpcpropd  15477  curfuncf  15507  curf2ndf  15516  yonffthlem  15551  acsfiindd  15807  mndpropd  15946  mhmeql  15995  isgrpinv  16100  mhmmnd  16192  conjnmzb  16301  gass  16339  symgextf  16442  dfod2  16586  gexdvds  16604  sylow3lem2  16648  efgredlem  16765  efgredeu  16770  ghmcmn  16840  oddvdssubg  16861  dprdfcntz  17049  dprdfcntzOLD  17055  pgpfaclem3  17134  issrg  17159  isring  17202  dvdsrmul1  17302  issubdrg  17454  islmhm2  17684  lmhmeql  17701  lssacsex  17790  issubassa2  17994  opsrval  18139  isphl  18663  uvcf1  18823  lindfmm  18862  scmatmats  19013  smatvscl  19026  mdetunilem7  19120  gsummatr01lem4  19160  m2cpmfo  19257  decpmatmulsumfsupp  19274  pmatcollpw3fi1lem1  19287  pm2mpf1lem  19295  pm2mpf1  19300  mp2pm2mplem4  19310  pm2mpghm  19317  pm2mpmhmlem1  19319  pm2mpmhmlem2  19320  chfacfscmulfsupp  19360  chfacfpmmulfsupp  19364  cctop  19507  neiptoptop  19632  neiptopreu  19634  tgrest  19660  ordtrest2lem  19704  cnss1  19777  cncnp  19781  isnrm3  19860  uncmp  19903  cmpfi  19908  iuncon  19929  1stcrest  19954  subislly  19982  islly2  19985  cldllycmp  19996  lly1stc  19997  llycmpkgen2  20051  kgencn  20057  xkoccn  20120  ptcnplem  20122  pthaus  20139  txhaus  20148  txkgen  20153  xkohaus  20154  xkococnlem  20160  txcon  20190  regr1lem2  20241  kqreglem1  20242  reghmph  20294  nrmhmph  20295  trfil2  20388  ufileu  20420  flimopn  20476  flimcf  20483  fclscf  20526  ufilcmp  20533  cnpfcf  20542  cnextfun  20564  tgpmulg  20592  symgtgp  20600  tgpt0  20617  qustgplem  20619  ustex2sym  20719  ustex3sym  20720  trust  20732  restutop  20740  restutopopn  20741  ustuqtop2  20745  ustuqtop4  20747  utop3cls  20754  utopreg  20755  cstucnd  20787  ucncn  20788  trcfilu  20797  neipcfilu  20799  ismet2  20836  metequiv2  21013  metcnp  21044  metcnp2  21045  metcnpi3  21049  txmetcnp  21050  metusttoOLD  21060  metustto  21061  metustsymOLD  21064  metustsym  21065  metustOLD  21070  metust  21071  cfilucfilOLD  21072  cfilucfil  21073  metuel2  21082  metutopOLD  21085  psmetutop  21086  restmetu  21090  metucnOLD  21091  metucn  21092  ngptgp  21150  tngngp  21168  nmoleub  21238  icccmp  21330  reconnlem2  21332  reconn  21333  xmetdcn2  21342  metdseq0  21358  metdscn  21360  elcncf2  21394  cncfmet  21412  cnheibor  21455  nmoleub2lem2  21599  nmoleub3  21602  iscfil2  21705  iscfil3  21712  cfilfcls  21713  equivcfil  21738  caubl  21746  bcthlem5  21767  pmltpc  21862  ovollb2  21900  ovoliunnul  21918  ovolicc2lem4  21931  volsup  21966  ioorf  21982  dyadss  22003  dyaddisjlem  22004  mbfposr  22059  cncombf  22065  mbflimsup  22073  i1fmulclem  22109  mbfi1fseqlem4  22125  iblss2  22212  ellimc2  22281  ellimc3  22283  dvnadd  22332  dvmptfsum  22376  dvferm1  22386  dvferm2  22388  fta1g  22568  plyeq0lem  22607  plydivex  22693  fta1  22704  aalioulem2  22729  aalioulem3  22730  ulmuni  22787  ulmbdd  22793  ulmdvlem3  22797  mtest  22799  abelthlem8  22834  pilem3  22848  efopn  23039  cxpmul2z  23072  cxpcn3lem  23121  jensen  23318  isppw2  23389  sqf11  23413  mersenne  23502  dchrelbas3  23513  dchrptlem1  23539  dchrpt  23542  lgsval2lem  23581  lgsdchrval  23622  lgsquad3  23636  2sqb  23653  pntrsumbnd2  23752  pntpbnd  23773  pntibnd  23778  istrkgc  23851  istrkgb  23852  tglowdim1i  23892  tgbtwndiff  23897  tgifscgr  23900  tgcgrxfr  23909  lnext  23954  tgbtwnconn1lem3  23961  tgbtwnconn1  23962  legval  23971  legov  23972  legov2  23973  legtrd  23976  legtri3  23977  legso  23985  tglnne  24008  tglndim0  24009  tglineeltr  24011  tglinethru  24016  tglnne0  24020  tglnpt2  24021  colline  24030  tglowdim2l  24031  tglowdim2ln  24032  mirreu3  24035  miriso  24050  midexlem  24069  isperp  24089  perpcom  24090  perpneq  24091  isperp2  24092  footex  24095  colperpexlem3  24106  opphllem  24109  midex  24111  opptgdim2  24117  opphllem2  24120  opphllem3  24121  opphllem5  24123  opphllem6  24124  opphl  24125  lnopp2hpgb  24132  lmieu  24150  f1otrg  24174  f1otrge  24175  axsegcon  24230  axeuclidlem  24265  axcontlem2  24268  usgra1  24373  usgrares1  24410  nbgraf1olem5  24445  pthdepisspth  24576  clwwlkf1  24796  clwwlknscsh  24819  el2spthonot  24870  usg2wotspth  24884  iseupa  24965  eupath2  24980  frgrancvvdeqlem9  25041  friendshipgt3  25121  isgrp2d  25237  smcnlem  25607  0lno  25705  ubthlem1  25786  ubthlem3  25788  chocunii  26219  occl  26222  5oalem1  26572  3oalem2  26581  nmopub2tALT  26828  nmfnleub2  26845  lnconi  26952  kbass5  27039  mdslmd1lem1  27244  mdslmd1lem2  27245  cdj1i  27352  disjabrex  27443  disjabrexf  27444  fgreu  27513  xrge0infss  27580  xrofsup  27582  2sqmo  27637  ressprs  27643  xrge0addgt0  27681  submarchi  27730  isarchi3  27731  archiabllem1  27737  archiabllem2a  27738  gsumle  27770  suborng  27805  isarchiofld  27807  fimaproj  27836  txomap  27837  qtophaus  27839  cmpcref  27853  pstmxmet  27876  sqsscirc1  27890  ordtrest2NEWlem  27904  ordtconlem1  27906  pnfneige0  27933  lmxrge0  27934  lmdvg  27935  qqhval2  27963  esumcst  28071  esumfsup  28076  esumcvg  28092  sigaclfu2  28121  insiga  28137  measinb  28192  imambfm  28233  oms0  28266  eulerpartlemgvv  28315  dstrvprob  28410  sgnsub  28483  signstfvneq0  28529  afsval  28551  lgambdd  28579  lgamucov  28580  derangenlem  28615  sconpi1  28684  cvmsss2  28719  cvmopnlem  28723  cvmlift3lem7  28770  msrval  28898  ifscgr  29694  cgrxfr  29705  btwnconn1lem13  29749  outsideofeu  29781  heicant  30049  mblfinlem1  30051  itg2addnclem  30066  ftc1cnnc  30089  ftc1anclem7  30096  neibastop2lem  30178  sstotbnd2  30270  equivtotbnd  30274  isbnd3  30280  ssbnd  30284  totbndbnd  30285  cntotbnd  30292  heibor1lem  30305  rrncmslem  30328  mzpindd  30678  mzpsubst  30681  mzpcompact2lem  30684  eldioph2b  30696  irrapxlem3  30760  irrapxlem5  30762  pellex  30771  pell1234qrdich  30797  pell14qrexpcl  30803  congabseq  30912  jm2.26a  30942  jm2.26lem3  30943  rmydioph  30956  lnrfg  31068  hbt  31079  fnchoice  31404  cncmpmax  31407  climrec  31609  climsuse  31614  islptre  31625  addlimc  31654  0ellimcdiv  31655  icccncfext  31690  cncfiooicclem1  31696  fperdvper  31715  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvmptfprodlem  31741  dvmptfprod  31742  dvnprodlem2  31744  stoweidlem7  31789  stoweidlem34  31816  stoweidlem52  31834  stoweidlem60  31842  wallispilem3  31849  fourierdlem34  31923  fourierdlem38  31927  fourierdlem39  31928  fourierdlem48  31937  fourierdlem50  31939  fourierdlem51  31940  fourierdlem73  31962  fourierdlem76  31965  fourierdlem77  31966  fourierdlem80  31969  fourierdlem87  31976  fourierdlem103  31992  fourierdlem104  31993  etransclem32  32049  etransclem33  32050  usgra2pthspth  32351  mgmhmeql  32491  isrng  32682  2zlidl  32740  lindslinindsimp2  33064  snlindsntor  33072  lincresunit2  33079  islindeps2  33084  4an4132  33268  iunconlem2  33735  lssats  34737  lsat0cv  34758  lkrlss  34820  lfl1dim  34846  lfl1dim2N  34847  lkrpssN  34888  hlhgt2  35113  3dim2  35192  2dim  35194  lplncvrlvol  35340  paddasslem11  35554  pmapjat1  35577  2polssN  35639  pclfinclN  35674  pexmidlem8N  35701  lhpexle1lem  35731  4atex  35800  ltrnid  35859  trlator0  35896  cdlemg2cex  36317  tendodi1  36510  tendodi2  36511  diblss  36897  dihopelvalcpre  36975  dihatexv  37065  mapdval4N  37359
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