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

Theorem simprr1 1005
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 963 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )
)  ->  ph )
21adantl 453 1  |-  ( ( ta  /\  ( th 
/\  ( ph  /\  ps  /\  ch ) ) )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  sqrmo  11986  haust1  17340  cnhaus  17342  isreg2  17365  llynlly  17463  restnlly  17468  llyrest  17471  llyidm  17474  nllyidm  17475  cldllycmp  17481  txlly  17591  txnlly  17592  pthaus  17593  txhaus  17602  txkgen  17607  xkohaus  17608  xkococnlem  17614  hauspwpwf1  17942  itg2add  19520  ulmdvlem3  20187  conpcon  24703  cvmliftmolem2  24750  cvmlift2lem10  24780  cvmlift3lem2  24788  cvmlift3lem8  24794  ax5seglem6  25589  broutsideof3  25776  icodiamlt  26576  mpaaeu  27026  psgnunilem2  27089  stoweidlem35  27454  stoweidlem56  27475  stoweidlem59  27478  paddasslem10  29945  lhpexle2lem  30125  lhpexle3lem  30127  cdlemj3  30939  cdlemkid4  31050
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