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

Theorem simprr2 1032
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 990 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )
)  ->  ps )
21adantl 463 1  |-  ( ( ta  /\  ( th 
/\  ( ph  /\  ps  /\  ch ) ) )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 960
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 962
This theorem is referenced by:  psgnunilem2  15983  haust1  18800  cnhaus  18802  isreg2  18825  llynlly  18925  restnlly  18930  llyrest  18933  llyidm  18936  nllyidm  18937  cldllycmp  18943  txlly  19053  txnlly  19054  pthaus  19055  txhaus  19064  txkgen  19069  xkohaus  19070  xkococnlem  19076  cmetcaulem  20643  itg2add  21081  ulmdvlem3  21754  ax5seglem6  23005  conpcon  26974  cvmlift3lem2  27059  cvmlift3lem8  27065  broutsideof3  28006  icodiamlt  29008  stoweidlem35  29678  stoweidlem56  29699  stoweidlem59  29702  n4cyclfrgra  30458  numclwlk1lem2f  30533  paddasslem10  33086  lhpexle2lem  33266  lhpexle3lem  33268
  Copyright terms: Public domain W3C validator