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

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

Proof of Theorem simp2rr
StepHypRef Expression
1 simprr 734 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ps )
213ad2ant2 979 1  |-  ( ( th  /\  ( ch 
/\  ( ph  /\  ps ) )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  omeu  6828  gruina  8693  4sqlem18  13330  vdwlem10  13358  tsmsxp  18184  ax5seglem3  25870  btwnconn1lem1  26021  btwnconn1lem3  26023  btwnconn1lem4  26024  btwnconn1lem5  26025  btwnconn1lem6  26026  btwnconn1lem7  26027  btwnconn1lem12  26032  linethru  26087  pellex  26898  lmhmfgsplit  27161  2llnjN  30364  2lplnja  30416  2lplnj  30417  cdlemblem  30590  dalaw  30683  pclfinN  30697  lhpmcvr4N  30823  cdlemb2  30838  cdleme01N  31018  cdleme0ex2N  31021  cdleme7c  31042  cdlemefrs29bpre0  31193  cdlemefrs29cpre1  31195  cdlemefrs32fva1  31198  cdlemefs32sn1aw  31211  cdleme41sn3a  31230  cdleme48fv  31296  cdlemk21-2N  31688  dihmeetlem13N  32117
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