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  6583  hashbclem  11390  tsmsxp  17837  tgqioo  18306  ovolunlem2  18857  plyadd  19599  plymul  19600  coeeu  19607  gxmul  20945  cvmlift2lem10  23843  btwnconn1lem1  24710  btwnconn1lem2  24711  btwnconn1lem12  24721  injsurinj  25149  jm2.27  27101  lplnexllnN  29753  2llnjN  29756  4atlem12b  29800  lplncvrlvol2  29804  lncmp  29972  cdlema2N  29981  cdlemc2  30381  cdleme11a  30449  cdleme22eALTN  30534  cdleme24  30541  cdleme27a  30556  cdleme27N  30558  cdleme28  30562  cdlemefs29bpre0N  30605  cdlemefs29bpre1N  30606  cdlemefs29cpre1N  30607  cdlemefs29clN  30608  cdlemefs32fvaN  30611  cdlemefs32fva1  30612  cdleme36m  30650  cdleme39a  30654  cdleme17d3  30685  cdleme50trn2  30740  cdlemg36  30903  cdlemj3  31012  cdlemkfid1N  31110  cdlemkid1  31111  cdlemk19ylem  31119  cdlemk19xlem  31131  dihlsscpre  31424  dihord4  31448  dihatlat  31524  mapdh9a  31980
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