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

Theorem simp3rr 1073
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 760 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ps )
213ad2ant3 1022 1  |-  ( ( th  /\  ta  /\  ( ch  /\  ( ph  /\  ps ) ) )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 976
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 187  df-an 371  df-3an 978
This theorem is referenced by:  omeu  7273  ntrivcvgmul  13865  tsmsxp  20951  tgqioo  21599  ovolunlem2  22203  plyadd  22908  plymul  22909  coeeu  22916  tghilberti2  24407  cvmlift2lem10  29622  btwnconn1lem1  30438  lplnexllnN  32594  2llnjN  32597  4atlem12b  32641  lplncvrlvol2  32645  lncmp  32813  cdlema2N  32822  cdleme11a  33291  cdleme24  33384  cdleme28  33405  cdlemefr29bpre0N  33438  cdlemefr29clN  33439  cdlemefr32fvaN  33441  cdlemefr32fva1  33442  cdlemefs29bpre0N  33448  cdlemefs29bpre1N  33449  cdlemefs29cpre1N  33450  cdlemefs29clN  33451  cdlemefs32fvaN  33454  cdlemefs32fva1  33455  cdleme36m  33493  cdleme17d3  33528  cdlemg36  33746  cdlemj3  33855  cdlemkid1  33954  cdlemk19ylem  33962  cdlemk19xlem  33974  dihlsscpre  34267  dihord4  34291  dihmeetlem1N  34323  dihatlat  34367  jm2.27  35325
  Copyright terms: Public domain W3C validator