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

Theorem simp2rr 1058
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 756 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ps )
213ad2ant2 1010 1  |-  ( ( th  /\  ( ch 
/\  ( ph  /\  ps ) )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967
This theorem is referenced by:  tfrlem5  6837  omeu  7022  gruina  8983  4sqlem18  14021  vdwlem10  14049  mdetuni0  18425  mdetmul  18427  tsmsxp  19727  ax5seglem3  23175  btwnconn1lem1  28116  btwnconn1lem3  28118  btwnconn1lem4  28119  btwnconn1lem5  28120  btwnconn1lem6  28121  btwnconn1lem7  28122  btwnconn1lem12  28127  linethru  28182  pellex  29173  lmhmfgsplit  29436  2llnjN  33208  2lplnja  33260  2lplnj  33261  cdlemblem  33434  dalaw  33527  pclfinN  33541  lhpmcvr4N  33667  cdlemb2  33682  cdleme01N  33862  cdleme0ex2N  33865  cdleme7c  33886  cdlemefrs29bpre0  34037  cdlemefrs29cpre1  34039  cdlemefrs32fva1  34042  cdlemefs32sn1aw  34055  cdleme41sn3a  34074  cdleme48fv  34140  cdlemk21-2N  34532  dihmeetlem13N  34961
  Copyright terms: Public domain W3C validator