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

Theorem simp3lr 1060
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 754 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ps )
213ad2ant3 1011 1  |-  ( ( th  /\  ta  /\  ( ( ph  /\  ps )  /\  ch )
)  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  f1oiso2  6048  omeu  7029  tsmsxp  19734  tgqioo  20382  ovolunlem2  20986  plyadd  21690  plymul  21691  coeeu  21698  tghilbert1_2  23049  ntrivcvgmul  27422  btwnconn1lem2  28124  btwnconn1lem3  28125  btwnconn1lem4  28126  pellex  29181  jm2.27  29362  athgt  33105  2llnjN  33216  4atlem12b  33260  lncmp  33432  cdlema2N  33441  cdleme21ct  33978  cdleme24  34001  cdleme27a  34016  cdleme28  34022  cdleme42b  34127  cdlemf  34212  dihlsscpre  34884  dihord4  34908  dihord5apre  34912
  Copyright terms: Public domain W3C validator