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

Theorem simprr2 1054
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 1012 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )
)  ->  ps )
21adantl 467 1  |-  ( ( ta  /\  ( th 
/\  ( ph  /\  ps  /\  ch ) ) )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  psgnunilem2  17087  haust1  20299  cnhaus  20301  isreg2  20324  llynlly  20423  restnlly  20428  llyrest  20431  llyidm  20434  nllyidm  20435  cldllycmp  20441  txlly  20582  txnlly  20583  pthaus  20584  txhaus  20593  txkgen  20598  xkohaus  20599  xkococnlem  20605  cmetcaulem  22151  itg2add  22594  ulmdvlem3  23222  ax5seglem6  24810  n4cyclfrgra  25591  numclwlk1lem2f  25665  conpcon  29746  cvmlift3lem2  29831  cvmlift3lem8  29837  broutsideof3  30678  paddasslem10  33102  lhpexle2lem  33282  lhpexle3lem  33284  icodiamlt  35373  stoweidlem35  37464  stoweidlem56  37485  stoweidlem59  37488
  Copyright terms: Public domain W3C validator