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

Theorem simp3rr 1029
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 733 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ps )
213ad2ant3 978 1  |-  ( ( th  /\  ta  /\  ( ch  /\  ( ph  /\  ps ) ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  omeu  6599  tsmsxp  17853  tgqioo  18322  ovolunlem2  18873  plyadd  19615  plymul  19616  coeeu  19623  cvmlift2lem10  23858  btwnconn1lem1  24782  jm2.27  27204  lplnexllnN  30375  2llnjN  30378  4atlem12b  30422  lplncvrlvol2  30426  lncmp  30594  cdlema2N  30603  cdleme11a  31071  cdleme24  31163  cdleme28  31184  cdlemefr29bpre0N  31217  cdlemefr29clN  31218  cdlemefr32fvaN  31220  cdlemefr32fva1  31221  cdlemefs29bpre0N  31227  cdlemefs29bpre1N  31228  cdlemefs29cpre1N  31229  cdlemefs29clN  31230  cdlemefs32fvaN  31233  cdlemefs32fva1  31234  cdleme36m  31272  cdleme17d3  31307  cdlemg36  31525  cdlemj3  31634  cdlemkid1  31733  cdlemk19ylem  31741  cdlemk19xlem  31753  dihlsscpre  32046  dihord4  32070  dihmeetlem1N  32102  dihatlat  32146
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