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  11737  haust1  17080  cnhaus  17082  isreg2  17105  llynlly  17203  restnlly  17208  llyrest  17211  llyidm  17214  nllyidm  17215  cldllycmp  17221  txlly  17330  txnlly  17331  pthaus  17332  txhaus  17341  txkgen  17346  xkohaus  17347  xkococnlem  17353  hauspwpwf1  17682  itg2add  19114  ulmdvlem3  19779  conpcon  23766  cvmliftmolem2  23813  cvmlift2lem10  23843  cvmlift3lem2  23851  cvmlift3lem8  23857  ax5seglem6  24562  broutsideof3  24749  toplat  25290  bisig0  26062  icodiamlt  26905  mpaaeu  27355  psgnunilem2  27418  stoweidlem35  27784  stoweidlem56  27805  stoweidlem59  27808  paddasslem10  30018  lhpexle2lem  30198  lhpexle3lem  30200  cdlemj3  31012  cdlemkid4  31123
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