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

Theorem simp3lr 1029
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 732 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ps )
213ad2ant3 980 1  |-  ( ( th  /\  ta  /\  ( ( ph  /\  ps )  /\  ch )
)  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  f1oiso2  6039  omeu  6795  tsmsxp  18145  tgqioo  18792  ovolunlem2  19355  plyadd  20097  plymul  20098  coeeu  20105  ntrivcvgmul  25191  btwnconn1lem2  25934  btwnconn1lem3  25935  btwnconn1lem4  25936  pellex  26796  jm2.27  26977  athgt  29950  2llnjN  30061  4atlem12b  30105  lncmp  30277  cdlema2N  30286  cdleme21ct  30823  cdleme24  30846  cdleme27a  30861  cdleme28  30867  cdleme42b  30972  cdlemf  31057  dihlsscpre  31729  dihord4  31753  dihord5apre  31757
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