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

Theorem simprr2 1004
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simprr2  |-  ( ( ta  /\  ( th 
/\  ( ph  /\  ps  /\  ch ) ) )  ->  ps )

Proof of Theorem simprr2
StepHypRef Expression
1 simpr2 962 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )
)  ->  ps )
21adantl 452 1  |-  ( ( ta  /\  ( th 
/\  ( ph  /\  ps  /\  ch ) ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  haust1  17096  cnhaus  17098  isreg2  17121  llynlly  17219  restnlly  17224  llyrest  17227  llyidm  17230  nllyidm  17231  cldllycmp  17237  txlly  17346  txnlly  17347  pthaus  17348  txhaus  17357  txkgen  17362  xkohaus  17363  xkococnlem  17369  cmetcaulem  18730  itg2add  19130  ulmdvlem3  19795  conpcon  23781  cvmlift3lem2  23866  cvmlift3lem8  23872  ax5seglem6  24634  broutsideof3  24821  bisig0  26165  bosser  26270  icodiamlt  27008  psgnunilem2  27521  stoweidlem35  27887  stoweidlem56  27908  stoweidlem59  27911  n4cyclfrgra  28440  paddasslem10  30640  lhpexle2lem  30820  lhpexle3lem  30822
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator