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  6821  4sqlem18  13323  vdwlem10  13351  mvrf1  16482  tsmsxp  18177  ax5seglem3  25863  btwnconn1lem1  26014  btwnconn1lem3  26016  btwnconn1lem4  26017  btwnconn1lem5  26018  btwnconn1lem6  26019  btwnconn1lem7  26020  linethru  26080  pellex  26890  expmordi  27002  lshpkrlem6  29851  athgt  30191  2llnjN  30302  dalaw  30621  cdlemb2  30776  4atexlemex6  30809  cdleme01N  30956  cdleme0ex2N  30959  cdleme7aa  30977  cdleme7e  30982  cdlemg33c0  31437  dihmeetlem3N  32041
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