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  6787  tsmsxp  18137  tgqioo  18784  ovolunlem2  19347  plyadd  20089  plymul  20090  coeeu  20097  cvmlift2lem10  24952  ntrivcvgmul  25183  btwnconn1lem1  25925  jm2.27  26969  lplnexllnN  30046  2llnjN  30049  4atlem12b  30093  lplncvrlvol2  30097  lncmp  30265  cdlema2N  30274  cdleme11a  30742  cdleme24  30834  cdleme28  30855  cdlemefr29bpre0N  30888  cdlemefr29clN  30889  cdlemefr32fvaN  30891  cdlemefr32fva1  30892  cdlemefs29bpre0N  30898  cdlemefs29bpre1N  30899  cdlemefs29cpre1N  30900  cdlemefs29clN  30901  cdlemefs32fvaN  30904  cdlemefs32fva1  30905  cdleme36m  30943  cdleme17d3  30978  cdlemg36  31196  cdlemj3  31305  cdlemkid1  31404  cdlemk19ylem  31412  cdlemk19xlem  31424  dihlsscpre  31717  dihord4  31741  dihmeetlem1N  31773  dihatlat  31817
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