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

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

Proof of Theorem simprr2
StepHypRef Expression
1 simpr2 995 . 2
21adantl 466 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 965
This theorem is referenced by:  psgnunilem2  16160  haust1  19355  cnhaus  19357  isreg2  19380  llynlly  19480  restnlly  19485  llyrest  19488  llyidm  19491  nllyidm  19492  cldllycmp  19498  txlly  19608  txnlly  19609  pthaus  19610  txhaus  19619  txkgen  19624  xkohaus  19625  xkococnlem  19631  cmetcaulem  21198  itg2add  21637  ulmdvlem3  22267  ax5seglem6  23649  conpcon  27580  cvmlift3lem2  27665  cvmlift3lem8  27671  broutsideof3  28613  icodiamlt  29621  stoweidlem35  30564  stoweidlem56  30585  stoweidlem59  30588  n4cyclfrgra  31487  numclwlk1lem2f  31562  paddasslem10  34324  lhpexle2lem  34504  lhpexle3lem  34506
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