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

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

Proof of Theorem simprr2
StepHypRef Expression
1 simpr2 980 . 2
21adantl 456 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 362  /\w3a 950
This theorem is referenced by:  psgnunilem2  15938  haust1  18660  cnhaus  18662  isreg2  18685  llynlly  18785  restnlly  18790  llyrest  18793  llyidm  18796  nllyidm  18797  cldllycmp  18803  txlly  18913  txnlly  18914  pthaus  18915  txhaus  18924  txkgen  18929  xkohaus  18930  xkococnlem  18936  cmetcaulem  20499  itg2add  20937  ulmdvlem3  21608  ax5seglem6  22859  conpcon  26827  cvmlift3lem2  26912  cvmlift3lem8  26918  broutsideof3  27859  icodiamlt  28834  stoweidlem35  29504  stoweidlem56  29525  stoweidlem59  29528  n4cyclfrgra  30284  numclwlk1lem2f  30359  paddasslem10  32910  lhpexle2lem  33090  lhpexle3lem  33092
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 179  df-an 364  df-3an 952
  Copyright terms: Public domain W3C validator