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  17080  cnhaus  17082  isreg2  17105  llynlly  17203  restnlly  17208  llyrest  17211  llyidm  17214  nllyidm  17215  cldllycmp  17221  txlly  17330  txnlly  17331  pthaus  17332  txhaus  17341  txkgen  17346  xkohaus  17347  xkococnlem  17353  cmetcaulem  18714  itg2add  19114  ulmdvlem3  19779  conpcon  23766  cvmlift3lem2  23851  cvmlift3lem8  23857  ax5seglem6  24562  broutsideof3  24749  bisig0  26062  bosser  26167  icodiamlt  26905  psgnunilem2  27418  stoweidlem35  27784  stoweidlem56  27805  stoweidlem59  27808  paddasslem10  30018  lhpexle2lem  30198  lhpexle3lem  30200
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