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

Theorem simprr3 1005
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simprr3  |-  ( ( ta  /\  ( th 
/\  ( ph  /\  ps  /\  ch ) ) )  ->  ch )

Proof of Theorem simprr3
StepHypRef Expression
1 simpr3 963 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )
)  ->  ch )
21adantl 452 1  |-  ( ( ta  /\  ( th 
/\  ( ph  /\  ps  /\  ch ) ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  haust1  17096  cnhaus  17098  isreg2  17121  llynlly  17219  restnlly  17224  llyrest  17227  llyidm  17230  nllyidm  17231  cldllycmp  17237  txlly  17346  txnlly  17347  pthaus  17348  txhaus  17357  txkgen  17362  xkohaus  17363  xkococnlem  17369  cmetcaulem  18730  itg2add  19130  ulmdvlem3  19795  conpcon  23781  cvmlift3lem2  23866  cvmlift3lem8  23872  ax5seglem6  24634  ifscgr  24739  broutsideof3  24821  bisig0  26165  bosser  26270  icodiamlt  27008  mpaaeu  27458  psgnunilem2  27521  stoweidlem35  27887  stoweidlem56  27908  stoweidlem59  27911  paddasslem10  30640  lhpexle2lem  30820  lhpexle3lem  30822
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator