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

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

Proof of Theorem simprr1
StepHypRef Expression
1 simpr1 961 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )
)  ->  ph )
21adantl 452 1  |-  ( ( ta  /\  ( th 
/\  ( ph  /\  ps  /\  ch ) ) )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  sqrmo  11753  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  hauspwpwf1  17698  itg2add  19130  ulmdvlem3  19795  conpcon  23781  cvmliftmolem2  23828  cvmlift2lem10  23858  cvmlift3lem2  23866  cvmlift3lem8  23872  ax5seglem6  24634  broutsideof3  24821  toplat  25393  bisig0  26165  icodiamlt  27008  mpaaeu  27458  psgnunilem2  27521  stoweidlem35  27887  stoweidlem56  27908  stoweidlem59  27911  paddasslem10  30640  lhpexle2lem  30820  lhpexle3lem  30822  cdlemj3  31634  cdlemkid4  31745
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