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

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

Proof of Theorem simplll
StepHypRef Expression
1 simpl 457 . 2
21ad2antrr 725 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  simp-4l  767  f1imass  6172  oeeui  7270  oaabs2  7313  boxcutc  7532  omxpenlem  7638  cantnfle  8111  cantnfleOLD  8141  acndom2  8456  infpwfien  8464  sornom  8678  isf32lem2  8755  isf32lem4  8757  fin1a2lem11  8811  ttukeylem5  8914  pwfseq  9063  gchina  9098  inttsk  9173  inar1  9174  prlem936  9446  mulcmpblnr  9469  00id  9776  mul02lem1  9777  addid1  9781  cnegex  9782  negeu  9833  add20  10089  ltmul12a  10423  lediv12a  10463  cru  10553  qextltlem  11430  xmullem  11485  xlemul1a  11509  ixxss12  11578  ioodisj  11679  elfz0fzfz0  11808  fsuppmapnn0fz  12102  seqf1o  12148  mulexpz  12206  leexp1a  12224  seqcoll  12512  swrdswrdlem  12684  abs3lem  13171  cau3lem  13187  climcau  13493  sumeq2ii  13515  summolem2  13538  climcndslem1  13661  climcndslem2  13662  geomulcvg  13685  mertenslem1  13693  mertenslem2  13694  mertens  13695  prodeq2ii  13720  prodmolem2  13742  bitsfzo  14085  sadadd2lem2  14100  dvdsmulgcd  14192  qredeu  14248  pc2dvds  14402  pcz  14404  ramcl  14547  firest  14830  mreexexlemd  15041  isacs2  15050  iscatd2  15078  ipodrsima  15795  mrelatlub  15816  mndpropd  15946  mhmeql  15995  isgrpinv  16100  mulgnn0dir  16165  mhmid  16191  mhmmnd  16192  issubg4  16220  gasubg  16340  symgextf  16442  pmtr3ncom  16500  gexdvds  16604  oddvdssubg  16861  cyggeninv  16886  cyggenod  16887  issrg  17159  dvdsrmul1  17302  unitgrp  17316  cntzsubr  17461  islmhm2  17684  lmhmeql  17701  lbspropd  17745  lssacsex  17790  issubassa2  17994  mplbas2  18134  mplbas2OLD  18135  psgndiflemA  18637  isphl  18663  ocvocv  18702  lindfmm  18862  scmatmats  19013  smatvscl  19026  mdetdiag  19101  m2cpmfo  19257  pmatcollpw3fi1lem1  19287  pm2mpf1  19300  pm2mpghm  19317  fvmptnn04if  19350  chfacfscmulfsupp  19360  chfacfpmmulfsupp  19364  neissex  19628  neiptoptop  19632  neiptopnei  19633  restbas  19659  tgrest  19660  restopnb  19676  cnpco  19768  isnrm3  19860  isreg2  19878  iuncon  19929  1stcrest  19954  2ndcctbss  19956  2ndcomap  19959  2ndcsep  19960  dislly  19998  kgencn2  20058  ptbasfi  20082  txhaus  20148  txkgen  20153  txcon  20190  qtopcn  20215  regr1lem2  20241  kqnrmlem1  20244  kqnrmlem2  20245  trfbas2  20344  trfil2  20388  flimcf  20483  hauspwpwf1  20488  fclscf  20526  flimfnfcls  20529  cnextcn  20567  ustexsym  20718  ustex2sym  20719  ustex3sym  20720  ustuqtop4  20747  utop3cls  20754  utopreg  20755  ucnima  20784  ucncn  20788  fmucnd  20795  metequiv2  21013  prdsxmslem2  21032  metcnpi3  21049  metusttoOLD  21060  metustto  21061  metustidOLD  21062  metustid  21063  metustexhalfOLD  21066  metustexhalf  21067  ngptgp  21150  xrsblre  21316  icccmp  21330  reconnlem1  21331  reconn  21333  opnreen  21336  metdsf  21352  metdscn  21360  fsumcn  21374  elcncf2  21394  cncfmet  21412  pcoass  21524  lmcau  21751  rrxdstprj1  21836  pmltpc  21862  ivthlem2  21864  ivthlem3  21865  ovollb2  21900  volsup  21966  ioombl1  21972  ioorf  21982  dyadss  22003  dyaddisjlem  22004  dyadmax  22007  volcn  22015  cncombf  22065  mbflimsup  22073  itg2const2  22148  iblss2  22212  cpnord  22338  dvmptfsum  22376  fta1g  22568  plydivex  22693  fta1  22704  aannenlem1  22724  ulmdvlem3  22797  abelthlem8  22834  pilem3  22848  advlogexp  23036  cxpmul2z  23072  atantayl2  23269  jensen  23318  isppw2  23389  lgsqr  23621  lgsdchrval  23622  lgsquad3  23636  2sqb  23653  dchrisumlem3  23676  rpvmasum2  23697  mulog2sumlem2  23720  pntrsumbnd2  23752  f1otrg  24174  f1otrge  24175  axsegcon  24230  axeuclidlem  24265  axcontlem9  24275  eengtrkg  24288  nbgraf1olem5  24445  cusgrasize2inds  24477  0wlkon  24549  0trlon  24550  0pthon  24581  3v3e3cycl2  24664  wlkiswwlk1  24690  usg2wotspth  24884  vdiscusgra  24921  iseupa  24965  vdn1frgrav2  25025  vdgn1frgrav2  25026  frgrancvvdeqlem9  25041  frgrawopreg  25049  frghash2spot  25063  numclwlk1lem2foa  25091  numclwlk1lem2fo  25095  frgrareggt1  25116  vacn  25604  smcnlem  25607  0lno  25705  chocunii  26219  occl  26222  5oalem1  26572  3oalem2  26581  unoplin  26839  hmoplin  26861  lnconi  26952  kbass5  27039  mdslmd1lem1  27244  mdslmd1lem2  27245  mdsymlem2  27323  cdj1i  27352  disjabrex  27443  disjabrexf  27444  fgreu  27513  xrge0infss  27580  xrofsup  27582  xrge0addgt0  27681  submomnd  27700  submarchi  27730  archiabllem1  27737  archiabllem2a  27738  isarchiofld  27807  locfinreflem  27843  rge0scvg  27931  lmxrge0  27934  lmdvg  27935  qqhval2  27963  esumfsup  28076  esumpcvgval  28084  esumcvg  28092  sigaclfu2  28121  sigainb  28136  insiga  28137  measinblem  28191  measinb  28192  measdivcstOLD  28195  measdivcst  28196  oddpwdc  28293  dstrvprob  28410  sgnmul  28481  sgnsub  28483  signsply0  28508  signstfvneq0  28529  ptpcon  28678  sconpi1  28684  rescon  28691  cvmliftmolem2  28727  cvmlift2lem12  28759  poseq  29333  ifscgr  29694  cgrxfr  29705  outsideofeu  29781  linethru  29803  fin2so  30040  mblfinlem2  30052  mblfinlem3  30053  itg2addnclem  30066  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  neibastop1  30177  ssbnd  30284  totbndbnd  30285  prtlem10  30606  mzpsubst  30681  mzpcompact2lem  30684  eldioph2  30695  eldioph2b  30696  diophren  30747  pell14qrexpcl  30803  elpell1qr2  30808  monotoddzzfi  30878  acongtr  30916  acongrep  30918  jm2.19lem4  30934  jm2.26a  30942  jm2.26lem3  30943  jm2.26  30944  isnumbasgrplem2  31053  mendassa  31143  prmunb2  31191  adant423  31425  mullimc  31622  mullimcf  31629  neglimc  31653  icccncfext  31690  cncfiooicclem1  31696  fprodcncf  31704  dvnprodlem3  31745  iblcncfioo  31777  itgspltprt  31778  stoweidlem7  31789  stoweidlem28  31810  stoweidlem34  31816  stoweidlem48  31830  stoweidlem52  31834  wallispilem3  31849  fourierdlem12  31901  fourierdlem38  31927  fourierdlem39  31928  fourierdlem42  31931  fourierdlem46  31935  fourierdlem48  31937  fourierdlem49  31938  fourierdlem50  31939  fourierdlem51  31940  fourierdlem65  31954  fourierdlem73  31962  fourierdlem76  31965  fourierdlem87  31976  fourierdlem103  31992  fourierdlem104  31993  ralxfrd2  32303  mgmhmeql  32491  4an4132  33268  bnj1408  34092  lssats  34737  lkrlss  34820  lshpset2N  34844  2dim  35194  islvol5  35303  paddasslem11  35554  pexmidlem8N  35701  ltrnid  35859  idltrn  35874  trlator0  35896  trlnidatb  35902  cdlemf2  36288  cdlemg2cex  36317  tendodi1  36510  tendodi2  36511  diblss  36897  dihopelvalcpre  36975  dih1dimatlem  37056  dihglblem6  37067
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