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

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

Proof of Theorem simplr2
StepHypRef Expression
1 simpr2 1003 . 2
21adantr 465 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  soltmin  5411  frfi  7785  wemappo  7995  iccsplit  11682  ccatswrd  12681  pcdvdstr  14399  vdwlem12  14510  iscatd2  15078  oppccomfpropd  15122  resssetc  15419  resscatc  15432  mod1ile  15735  mod2ile  15736  prdsmndd  15953  grprcan  16083  mulgnn0dir  16165  mulgnn0di  16834  mulgdi  16835  lmodprop2d  17572  lssintcl  17610  prdslmodd  17615  islmhm2  17684  islbs3  17801  mdetmul  19125  restopnb  19676  nrmsep  19858  iuncon  19929  ptpjopn  20113  blsscls2  21007  xrsblre  21316  icccmplem2  21328  icccvx  21450  colline  24030  tglowdim2ln  24032  f1otrg  24174  f1otrge  24175  ax5seglem5  24236  axcontlem3  24269  axcontlem4  24270  axcontlem8  24274  eengtrkg  24288  erclwwlktr  24815  erclwwlkntr  24827  el2wlkonotot0  24872  extwwlkfablem1  25074  xrofsup  27582  submomnd  27700  ogrpaddltbi  27709  erdszelem8  28642  cvmliftmolem2  28727  cvmlift2lem12  28759  btwnswapid  29667  btwnsegle  29767  broutsideof3  29776  outsidele  29782  mendlmod  31142  mendassa  31143  3adantlr3  31417  ioondisj2  31525  ioondisj1  31526  stoweidlem60  31842  ply1mulgsumlem2  32987  lincresunit3lem2  33081  cvrletrN  34998  ltltncvr  35147  atcvrj2b  35156  cvrat4  35167  2at0mat0  35249  islpln2a  35272  paddasslem11  35554  pmod1i  35572  lautcvr  35816  cdlemg4c  36338  tendoplass  36509  tendodi1  36510  tendodi2  36511
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 975
  Copyright terms: Public domain W3C validator