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

Theorem simp2lr 1026
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 733 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ps )
213ad2ant2 980 1  |-  ( ( th  /\  ( (
ph  /\  ps )  /\  ch )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  omeu  6831  4sqlem18  13335  vdwlem10  13363  mvrf1  16494  tsmsxp  18189  ax5seglem3  25875  btwnconn1lem1  26026  btwnconn1lem3  26028  btwnconn1lem4  26029  btwnconn1lem5  26030  btwnconn1lem6  26031  btwnconn1lem7  26032  linethru  26092  pellex  26912  expmordi  27024  lshpkrlem6  29987  athgt  30327  2llnjN  30438  dalaw  30757  cdlemb2  30912  4atexlemex6  30945  cdleme01N  31092  cdleme0ex2N  31095  cdleme7aa  31113  cdleme7e  31118  cdlemg33c0  31573  dihmeetlem3N  32177
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator