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

Theorem simp3rl 1028
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp3rl  |-  ( ( th  /\  ta  /\  ( ch  /\  ( ph  /\  ps ) ) )  ->  ph )

Proof of Theorem simp3rl
StepHypRef Expression
1 simprl 732 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ph )
213ad2ant3 978 1  |-  ( ( th  /\  ta  /\  ( ch  /\  ( ph  /\  ps ) ) )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  omeu  6579  hashbclem  11386  tsmsxp  17833  tgqioo  18302  ovolunlem2  18853  plyadd  19595  plymul  19596  coeeu  19603  gxmul  20939  cvmlift2lem10  23250  btwnconn1lem1  24120  btwnconn1lem2  24121  btwnconn1lem12  24131  injsurinj  24560  jm2.27  26512  lplnexllnN  29032  2llnjN  29035  4atlem12b  29079  lplncvrlvol2  29083  lncmp  29251  cdlema2N  29260  cdlemc2  29660  cdleme11a  29728  cdleme22eALTN  29813  cdleme24  29820  cdleme27a  29835  cdleme27N  29837  cdleme28  29841  cdlemefs29bpre0N  29884  cdlemefs29bpre1N  29885  cdlemefs29cpre1N  29886  cdlemefs29clN  29887  cdlemefs32fvaN  29890  cdlemefs32fva1  29891  cdleme36m  29929  cdleme39a  29933  cdleme17d3  29964  cdleme50trn2  30019  cdlemg36  30182  cdlemj3  30291  cdlemkfid1N  30389  cdlemkid1  30390  cdlemk19ylem  30398  cdlemk19xlem  30410  dihlsscpre  30703  dihord4  30727  dihatlat  30803  mapdh9a  31259
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