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  12012  haust1  17370  cnhaus  17372  isreg2  17395  llynlly  17493  restnlly  17498  llyrest  17501  llyidm  17504  nllyidm  17505  cldllycmp  17511  txlly  17621  txnlly  17622  pthaus  17623  txhaus  17632  txkgen  17637  xkohaus  17638  xkococnlem  17644  hauspwpwf1  17972  itg2add  19604  ulmdvlem3  20271  conpcon  24875  cvmliftmolem2  24922  cvmlift2lem10  24952  cvmlift3lem2  24960  cvmlift3lem8  24966  ax5seglem6  25777  broutsideof3  25964  icodiamlt  26773  mpaaeu  27223  psgnunilem2  27286  stoweidlem35  27651  stoweidlem56  27672  stoweidlem59  27675  frg2woteqm  28162  paddasslem10  30311  lhpexle2lem  30491  lhpexle3lem  30493  cdlemj3  31305  cdlemkid4  31416
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