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

Theorem simp2rr 1066
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 757 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ps )
213ad2ant2 1018 1  |-  ( ( th  /\  ( ch 
/\  ( ph  /\  ps ) )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 975
This theorem is referenced by:  tfrlem5  7067  omeu  7252  gruina  9213  4sqlem18  14492  vdwlem10  14520  mdetuni0  19250  mdetmul  19252  tsmsxp  20783  ax5seglem3  24361  btwnconn1lem1  29921  btwnconn1lem3  29923  btwnconn1lem4  29924  btwnconn1lem5  29925  btwnconn1lem6  29926  btwnconn1lem7  29927  btwnconn1lem12  29932  linethru  29987  pellex  30954  lmhmfgsplit  31215  2llnjN  35413  2lplnja  35465  2lplnj  35466  cdlemblem  35639  dalaw  35732  pclfinN  35746  lhpmcvr4N  35872  cdlemb2  35887  cdleme01N  36068  cdleme0ex2N  36071  cdleme7c  36092  cdlemefrs29bpre0  36244  cdlemefrs29cpre1  36246  cdlemefrs32fva1  36249  cdlemefs32sn1aw  36262  cdleme41sn3a  36281  cdleme48fv  36347  cdlemk21-2N  36739  dihmeetlem13N  37168
  Copyright terms: Public domain W3C validator