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

Theorem simprr2 1006
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 964 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )
)  ->  ps )
21adantl 453 1  |-  ( ( ta  /\  ( th 
/\  ( ph  /\  ps  /\  ch ) ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  haust1  17416  cnhaus  17418  isreg2  17441  llynlly  17540  restnlly  17545  llyrest  17548  llyidm  17551  nllyidm  17552  cldllycmp  17558  txlly  17668  txnlly  17669  pthaus  17670  txhaus  17679  txkgen  17684  xkohaus  17685  xkococnlem  17691  cmetcaulem  19241  itg2add  19651  ulmdvlem3  20318  conpcon  24922  cvmlift3lem2  25007  cvmlift3lem8  25013  ax5seglem6  25873  broutsideof3  26060  icodiamlt  26883  psgnunilem2  27395  stoweidlem35  27760  stoweidlem56  27781  stoweidlem59  27784  n4cyclfrgra  28408  paddasslem10  30626  lhpexle2lem  30806  lhpexle3lem  30808
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator