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

Theorem simp3rr 1031
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 734 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ps )
213ad2ant3 980 1  |-  ( ( th  /\  ta  /\  ( ch  /\  ( ph  /\  ps ) ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  omeu  6820  tsmsxp  18176  tgqioo  18823  ovolunlem2  19386  plyadd  20128  plymul  20129  coeeu  20136  cvmlift2lem10  24991  ntrivcvgmul  25222  btwnconn1lem1  26013  jm2.27  27060  lplnexllnN  30288  2llnjN  30291  4atlem12b  30335  lplncvrlvol2  30339  lncmp  30507  cdlema2N  30516  cdleme11a  30984  cdleme24  31076  cdleme28  31097  cdlemefr29bpre0N  31130  cdlemefr29clN  31131  cdlemefr32fvaN  31133  cdlemefr32fva1  31134  cdlemefs29bpre0N  31140  cdlemefs29bpre1N  31141  cdlemefs29cpre1N  31142  cdlemefs29clN  31143  cdlemefs32fvaN  31146  cdlemefs32fva1  31147  cdleme36m  31185  cdleme17d3  31220  cdlemg36  31438  cdlemj3  31547  cdlemkid1  31646  cdlemk19ylem  31654  cdlemk19xlem  31666  dihlsscpre  31959  dihord4  31983  dihmeetlem1N  32015  dihatlat  32059
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator