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

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

Proof of Theorem simp2lr
StepHypRef Expression
1 simplr 754 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ps )
213ad2ant2 1018 1  |-  ( ( th  /\  ( (
ph  /\  ps )  /\  ch )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975
This theorem is referenced by:  tfrlem5  7061  omeu  7246  4sqlem18  14356  vdwlem10  14384  mvrf1  17951  mdetuni0  18992  mdetmul  18994  tsmsxp  20525  ax5seglem3  24048  btwnconn1lem1  29655  btwnconn1lem3  29657  btwnconn1lem4  29658  btwnconn1lem5  29659  btwnconn1lem6  29660  btwnconn1lem7  29661  linethru  29721  pellex  30690  expmordi  30802  lshpkrlem6  34268  athgt  34608  2llnjN  34719  dalaw  35038  cdlemb2  35193  4atexlemex6  35226  cdleme01N  35373  cdleme0ex2N  35376  cdleme7aa  35394  cdleme7e  35399  cdlemg33c0  35854  dihmeetlem3N  36458
  Copyright terms: Public domain W3C validator