MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp3rr 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  6765  tsmsxp  18106  tgqioo  18703  ovolunlem2  19262  plyadd  20004  plymul  20005  coeeu  20012  cvmlift2lem10  24779  ntrivcvgmul  25010  btwnconn1lem1  25736  jm2.27  26771  lplnexllnN  29679  2llnjN  29682  4atlem12b  29726  lplncvrlvol2  29730  lncmp  29898  cdlema2N  29907  cdleme11a  30375  cdleme24  30467  cdleme28  30488  cdlemefr29bpre0N  30521  cdlemefr29clN  30522  cdlemefr32fvaN  30524  cdlemefr32fva1  30525  cdlemefs29bpre0N  30531  cdlemefs29bpre1N  30532  cdlemefs29cpre1N  30533  cdlemefs29clN  30534  cdlemefs32fvaN  30537  cdlemefs32fva1  30538  cdleme36m  30576  cdleme17d3  30611  cdlemg36  30829  cdlemj3  30938  cdlemkid1  31037  cdlemk19ylem  31045  cdlemk19xlem  31057  dihlsscpre  31350  dihord4  31374  dihmeetlem1N  31406  dihatlat  31450
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