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  6599  hashbclem  11406  tsmsxp  17853  tgqioo  18322  ovolunlem2  18873  plyadd  19615  plymul  19616  coeeu  19623  gxmul  20961  cvmlift2lem10  23858  btwnconn1lem1  24782  btwnconn1lem2  24783  btwnconn1lem12  24793  injsurinj  25252  jm2.27  27204  lplnexllnN  30375  2llnjN  30378  4atlem12b  30422  lplncvrlvol2  30426  lncmp  30594  cdlema2N  30603  cdlemc2  31003  cdleme11a  31071  cdleme22eALTN  31156  cdleme24  31163  cdleme27a  31178  cdleme27N  31180  cdleme28  31184  cdlemefs29bpre0N  31227  cdlemefs29bpre1N  31228  cdlemefs29cpre1N  31229  cdlemefs29clN  31230  cdlemefs32fvaN  31233  cdlemefs32fva1  31234  cdleme36m  31272  cdleme39a  31276  cdleme17d3  31307  cdleme50trn2  31362  cdlemg36  31525  cdlemj3  31634  cdlemkfid1N  31732  cdlemkid1  31733  cdlemk19ylem  31741  cdlemk19xlem  31753  dihlsscpre  32046  dihord4  32070  dihatlat  32146  mapdh9a  32602
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