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

Theorem simplr2 1031
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simplr2

Proof of Theorem simplr2
StepHypRef Expression
1 simpr2 995 . 2
21adantr 465 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 965
This theorem is referenced by:  soltmin  5319  frfi  7642  wemappo  7848  iccsplit  11503  ccatswrd  12436  pcdvdstr  14028  vdwlem12  14139  iscatd2  14705  oppccomfpropd  14752  resssetc  15046  resscatc  15059  mod1ile  15361  mod2ile  15362  prdsmndd  15540  grprcan  15657  mulgnn0dir  15736  mulgnn0di  16401  mulgdi  16402  lmodprop2d  17097  lssintcl  17135  prdslmodd  17140  islmhm2  17209  islbs3  17326  mdetmul  18529  restopnb  18879  nrmsep  19061  iuncon  19132  ptpjopn  19285  blsscls2  20179  xrsblre  20488  icccmplem2  20500  icccvx  20622  colline  23161  tglowdim2ln  23163  f1otrg  23236  f1otrge  23237  ax5seglem5  23298  axcontlem3  23331  axcontlem4  23332  axcontlem8  23336  eengtrkg  23350  xrofsup  26173  submomnd  26291  ogrpaddltbi  26300  erdszelem8  27204  cvmliftmolem2  27289  cvmlift2lem12  27321  btwnswapid  28166  btwnsegle  28266  broutsideof3  28275  outsidele  28281  mendlmod  29672  mendassa  29673  stoweidlem60  29977  el2wlkonotot0  30513  erclwwlktr  30607  erclwwlkntr  30623  ply1mulgsumlem2  30971  lincresunit3lem2  31105  cvrletrN  33199  ltltncvr  33348  atcvrj2b  33357  cvrat4  33368  2at0mat0  33450  islpln2a  33473  paddasslem11  33755  pmod1i  33773  lautcvr  34017  cdlemg4c  34537  tendoplass  34708  tendodi1  34709  tendodi2  34710
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  df-3an 967
  Copyright terms: Public domain W3C validator