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

Theorem simp3lr 1068
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 1019 1  |-  ( ( th  /\  ta  /\  ( ( ph  /\  ps )  /\  ch )
)  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 975
This theorem is referenced by:  f1oiso2  6247  omeu  7246  tsmsxp  20523  tgqioo  21171  ovolunlem2  21775  plyadd  22480  plymul  22481  coeeu  22488  tghilbert1_2  23877  ntrivcvgmul  28970  btwnconn1lem2  29672  btwnconn1lem3  29673  btwnconn1lem4  29674  pellex  30705  jm2.27  30884  athgt  34658  2llnjN  34769  4atlem12b  34813  lncmp  34985  cdlema2N  34994  cdleme21ct  35531  cdleme24  35554  cdleme27a  35569  cdleme28  35575  cdleme42b  35680  cdlemf  35765  dihlsscpre  36437  dihord4  36461  dihord5apre  36465
  Copyright terms: Public domain W3C validator