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

Theorem simp3rl 1030
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 733 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ph )
213ad2ant3 980 1  |-  ( ( th  /\  ta  /\  ( ch  /\  ( ph  /\  ps ) ) )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  omeu  6764  hashbclem  11628  tsmsxp  18105  tgqioo  18702  ovolunlem2  19261  plyadd  20003  plymul  20004  coeeu  20011  gxmul  21714  cvmlift2lem10  24778  ntrivcvgmul  25009  btwnconn1lem1  25735  btwnconn1lem2  25736  btwnconn1lem12  25746  jm2.27  26770  lplnexllnN  29678  2llnjN  29681  4atlem12b  29725  lplncvrlvol2  29729  lncmp  29897  cdlema2N  29906  cdlemc2  30306  cdleme11a  30374  cdleme22eALTN  30459  cdleme24  30466  cdleme27a  30481  cdleme27N  30483  cdleme28  30487  cdlemefs29bpre0N  30530  cdlemefs29bpre1N  30531  cdlemefs29cpre1N  30532  cdlemefs29clN  30533  cdlemefs32fvaN  30536  cdlemefs32fva1  30537  cdleme36m  30575  cdleme39a  30579  cdleme17d3  30610  cdleme50trn2  30665  cdlemg36  30828  cdlemj3  30937  cdlemkfid1N  31035  cdlemkid1  31036  cdlemk19ylem  31044  cdlemk19xlem  31056  dihlsscpre  31349  dihord4  31373  dihatlat  31449  mapdh9a  31905
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