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

Theorem simprr2 1037
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 995 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )
)  ->  ps )
21adantl 466 1  |-  ( ( ta  /\  ( th 
/\  ( ph  /\  ps  /\  ch ) ) )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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
This theorem is referenced by:  psgnunilem2  16001  haust1  18956  cnhaus  18958  isreg2  18981  llynlly  19081  restnlly  19086  llyrest  19089  llyidm  19092  nllyidm  19093  cldllycmp  19099  txlly  19209  txnlly  19210  pthaus  19211  txhaus  19220  txkgen  19225  xkohaus  19226  xkococnlem  19232  cmetcaulem  20799  itg2add  21237  ulmdvlem3  21867  ax5seglem6  23180  conpcon  27124  cvmlift3lem2  27209  cvmlift3lem8  27215  broutsideof3  28157  icodiamlt  29161  stoweidlem35  29830  stoweidlem56  29851  stoweidlem59  29854  n4cyclfrgra  30610  numclwlk1lem2f  30685  paddasslem10  33473  lhpexle2lem  33653  lhpexle3lem  33655
  Copyright terms: Public domain W3C validator