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

Theorem simp3lr 1030
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 733 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ps )
213ad2ant3 981 1  |-  ( ( th  /\  ta  /\  ( ( ph  /\  ps )  /\  ch )
)  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  f1oiso2  6075  omeu  6831  tsmsxp  18189  tgqioo  18836  ovolunlem2  19399  plyadd  20141  plymul  20142  coeeu  20149  ntrivcvgmul  25235  btwnconn1lem2  26027  btwnconn1lem3  26028  btwnconn1lem4  26029  pellex  26912  jm2.27  27093  athgt  30327  2llnjN  30438  4atlem12b  30482  lncmp  30654  cdlema2N  30663  cdleme21ct  31200  cdleme24  31223  cdleme27a  31238  cdleme28  31244  cdleme42b  31349  cdlemf  31434  dihlsscpre  32106  dihord4  32130  dihord5apre  32134
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator