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  6625  gruina  8485  4sqlem18  13056  vdwlem10  13084  tsmsxp  17889  ax5seglem3  24945  btwnconn1lem1  25096  btwnconn1lem3  25098  btwnconn1lem4  25099  btwnconn1lem5  25100  btwnconn1lem6  25101  btwnconn1lem7  25102  btwnconn1lem12  25107  linethru  25162  pellex  26068  lmhmfgsplit  26332  2llnjN  29574  2lplnja  29626  2lplnj  29627  cdlemblem  29800  dalaw  29893  pclfinN  29907  lhpmcvr4N  30033  cdlemb2  30048  cdleme01N  30228  cdleme0ex2N  30231  cdleme7c  30252  cdlemefrs29bpre0  30403  cdlemefrs29cpre1  30405  cdlemefrs32fva1  30408  cdlemefs32sn1aw  30421  cdleme41sn3a  30440  cdleme48fv  30506  cdlemk21-2N  30898  dihmeetlem13N  31327
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