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  6583  tsmsxp  17837  tgqioo  18306  ovolunlem2  18857  plyadd  19599  plymul  19600  coeeu  19607  cvmlift2lem10  23843  btwnconn1lem1  24710  jm2.27  27101  lplnexllnN  29753  2llnjN  29756  4atlem12b  29800  lplncvrlvol2  29804  lncmp  29972  cdlema2N  29981  cdleme11a  30449  cdleme24  30541  cdleme28  30562  cdlemefr29bpre0N  30595  cdlemefr29clN  30596  cdlemefr32fvaN  30598  cdlemefr32fva1  30599  cdlemefs29bpre0N  30605  cdlemefs29bpre1N  30606  cdlemefs29cpre1N  30607  cdlemefs29clN  30608  cdlemefs32fvaN  30611  cdlemefs32fva1  30612  cdleme36m  30650  cdleme17d3  30685  cdlemg36  30903  cdlemj3  31012  cdlemkid1  31111  cdlemk19ylem  31119  cdlemk19xlem  31131  dihlsscpre  31424  dihord4  31448  dihmeetlem1N  31480  dihatlat  31524
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