MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp3rl Structured version   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  6820  hashbclem  11693  tsmsxp  18176  tgqioo  18823  ovolunlem2  19386  plyadd  20128  plymul  20129  coeeu  20136  gxmul  21858  cvmlift2lem10  24991  ntrivcvgmul  25222  btwnconn1lem1  26013  btwnconn1lem2  26014  btwnconn1lem12  26024  jm2.27  27070  lplnexllnN  30298  2llnjN  30301  4atlem12b  30345  lplncvrlvol2  30349  lncmp  30517  cdlema2N  30526  cdlemc2  30926  cdleme11a  30994  cdleme22eALTN  31079  cdleme24  31086  cdleme27a  31101  cdleme27N  31103  cdleme28  31107  cdlemefs29bpre0N  31150  cdlemefs29bpre1N  31151  cdlemefs29cpre1N  31152  cdlemefs29clN  31153  cdlemefs32fvaN  31156  cdlemefs32fva1  31157  cdleme36m  31195  cdleme39a  31199  cdleme17d3  31230  cdleme50trn2  31285  cdlemg36  31448  cdlemj3  31557  cdlemkfid1N  31655  cdlemkid1  31656  cdlemk19ylem  31664  cdlemk19xlem  31676  dihlsscpre  31969  dihord4  31993  dihatlat  32069  mapdh9a  32525
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