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

Theorem simp2lr 1065
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 755 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ps )
213ad2ant2 1019 1  |-  ( ( th  /\  ( (
ph  /\  ps )  /\  ch )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 974
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 976
This theorem is referenced by:  tfrlem5  7051  omeu  7236  4sqlem18  14357  vdwlem10  14385  mvrf1  17955  mdetuni0  18996  mdetmul  18998  tsmsxp  20530  ax5seglem3  24106  btwnconn1lem1  29712  btwnconn1lem3  29714  btwnconn1lem4  29715  btwnconn1lem5  29716  btwnconn1lem6  29717  btwnconn1lem7  29718  linethru  29778  pellex  30746  expmordi  30858  lshpkrlem6  34580  athgt  34920  2llnjN  35031  dalaw  35350  cdlemb2  35505  4atexlemex6  35538  cdleme01N  35686  cdleme0ex2N  35689  cdleme7aa  35707  cdleme7e  35712  cdlemg33c0  36168  dihmeetlem3N  36772
  Copyright terms: Public domain W3C validator