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

Theorem simp2lr 1025
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 732 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ps )
213ad2ant2 979 1  |-  ( ( th  /\  ( (
ph  /\  ps )  /\  ch )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  omeu  6820  4sqlem18  13322  vdwlem10  13350  mvrf1  16481  tsmsxp  18176  ax5seglem3  25862  btwnconn1lem1  26013  btwnconn1lem3  26015  btwnconn1lem4  26016  btwnconn1lem5  26017  btwnconn1lem6  26018  btwnconn1lem7  26019  linethru  26079  pellex  26889  expmordi  27001  lshpkrlem6  29850  athgt  30190  2llnjN  30301  dalaw  30620  cdlemb2  30775  4atexlemex6  30808  cdleme01N  30955  cdleme0ex2N  30958  cdleme7aa  30976  cdleme7e  30981  cdlemg33c0  31436  dihmeetlem3N  32040
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