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  5849  omeu  6583  tsmsxp  17837  tgqioo  18306  ovolunlem2  18857  plyadd  19599  plymul  19600  coeeu  19607  btwnconn1lem2  24711  btwnconn1lem3  24712  btwnconn1lem4  24713  pellex  26920  jm2.27  27101  athgt  29645  2llnjN  29756  4atlem12b  29800  lncmp  29972  cdlema2N  29981  cdleme21ct  30518  cdleme24  30541  cdleme27a  30556  cdleme28  30562  cdleme42b  30667  cdlemf  30752  dihlsscpre  31424  dihord4  31448  dihord5apre  31452
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