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

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

Proof of Theorem simp3lr
StepHypRef Expression
1 simplr 731 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ps )
213ad2ant3 978 1  |-  ( ( th  /\  ta  /\  ( ( ph  /\  ps )  /\  ch )
)  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  f1oiso2  5933  omeu  6667  tsmsxp  17933  tgqioo  18402  ovolunlem2  18955  plyadd  19697  plymul  19698  coeeu  19705  ntrivcvgmul  24531  btwnconn1lem2  25270  btwnconn1lem3  25271  btwnconn1lem4  25272  pellex  26243  jm2.27  26424  athgt  29697  2llnjN  29808  4atlem12b  29852  lncmp  30024  cdlema2N  30033  cdleme21ct  30570  cdleme24  30593  cdleme27a  30608  cdleme28  30614  cdleme42b  30719  cdlemf  30804  dihlsscpre  31476  dihord4  31500  dihord5apre  31504
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