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

Theorem simprr2 1045
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 1003 . 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 973
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 975
This theorem is referenced by:  psgnunilem2  16323  haust1  19635  cnhaus  19637  isreg2  19660  llynlly  19760  restnlly  19765  llyrest  19768  llyidm  19771  nllyidm  19772  cldllycmp  19778  txlly  19888  txnlly  19889  pthaus  19890  txhaus  19899  txkgen  19904  xkohaus  19905  xkococnlem  19911  cmetcaulem  21478  itg2add  21917  ulmdvlem3  22547  ax5seglem6  23929  n4cyclfrgra  24710  numclwlk1lem2f  24785  conpcon  28336  cvmlift3lem2  28421  cvmlift3lem8  28427  broutsideof3  29369  icodiamlt  30376  stoweidlem35  31351  stoweidlem56  31372  stoweidlem59  31375  paddasslem10  34634  lhpexle2lem  34814  lhpexle3lem  34816
  Copyright terms: Public domain W3C validator