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

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

Proof of Theorem simp3rr
StepHypRef Expression
1 simprr 756 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ps )
213ad2ant3 1019 1  |-  ( ( th  /\  ta  /\  ( ch  /\  ( ph  /\  ps ) ) )  ->  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:  omeu  7231  tsmsxp  20392  tgqioo  21040  ovolunlem2  21644  plyadd  22349  plymul  22350  coeeu  22357  tghilbert1_2  23732  cvmlift2lem10  28397  ntrivcvgmul  28613  btwnconn1lem1  29314  jm2.27  30554  lplnexllnN  34360  2llnjN  34363  4atlem12b  34407  lplncvrlvol2  34411  lncmp  34579  cdlema2N  34588  cdleme11a  35056  cdleme24  35148  cdleme28  35169  cdlemefr29bpre0N  35202  cdlemefr29clN  35203  cdlemefr32fvaN  35205  cdlemefr32fva1  35206  cdlemefs29bpre0N  35212  cdlemefs29bpre1N  35213  cdlemefs29cpre1N  35214  cdlemefs29clN  35215  cdlemefs32fvaN  35218  cdlemefs32fva1  35219  cdleme36m  35257  cdleme17d3  35292  cdlemg36  35510  cdlemj3  35619  cdlemkid1  35718  cdlemk19ylem  35726  cdlemk19xlem  35738  dihlsscpre  36031  dihord4  36055  dihmeetlem1N  36087  dihatlat  36131
  Copyright terms: Public domain W3C validator