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

Theorem simp2rr 1025
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 733 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ps )
213ad2ant2 977 1  |-  ( ( th  /\  ( ch 
/\  ( ph  /\  ps ) )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  omeu  6583  gruina  8440  4sqlem18  13009  vdwlem10  13037  tsmsxp  17837  ax5seglem3  24559  btwnconn1lem1  24710  btwnconn1lem3  24712  btwnconn1lem4  24713  btwnconn1lem5  24714  btwnconn1lem6  24715  btwnconn1lem7  24716  btwnconn1lem12  24721  linethru  24776  limptlimpr2lem1  25574  pellex  26920  lmhmfgsplit  27184  2llnjN  29756  2lplnja  29808  2lplnj  29809  cdlemblem  29982  dalaw  30075  pclfinN  30089  lhpmcvr4N  30215  cdlemb2  30230  cdleme01N  30410  cdleme0ex2N  30413  cdleme7c  30434  cdlemefrs29bpre0  30585  cdlemefrs29cpre1  30587  cdlemefrs32fva1  30590  cdlemefs32sn1aw  30603  cdleme41sn3a  30622  cdleme48fv  30688  cdlemk21-2N  31080  dihmeetlem13N  31509
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator