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

Theorem simp3ll 1059
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp3ll  |-  ( ( th  /\  ta  /\  ( ( ph  /\  ps )  /\  ch )
)  ->  ph )

Proof of Theorem simp3ll
StepHypRef Expression
1 simpll 753 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )
213ad2ant3 1011 1  |-  ( ( th  /\  ta  /\  ( ( ph  /\  ps )  /\  ch )
)  ->  ph )
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  6055  omeu  7036  tsmsxp  19741  tgqioo  20389  ovolunlem2  20993  plyadd  21697  plymul  21698  coeeu  21705  tghilbert1_2  23056  ntrivcvgmul  27429  btwnconn1lem2  28131  btwnconn1lem3  28132  btwnconn1lem12  28141  pellex  29188  jm2.27  29369  athgt  33112  2llnjN  33223  4atlem12b  33267  lncmp  33439  cdlema2N  33448  cdlemc2  33848  cdleme5  33896  cdleme11a  33916  cdleme21ct  33985  cdleme21  33993  cdleme22eALTN  34001  cdleme24  34008  cdleme27cl  34022  cdleme27a  34023  cdleme28  34029  cdleme36a  34116  cdleme42b  34134  cdleme48fvg  34156  cdlemf  34219  cdlemk39  34572  cdlemkid1  34578  dihlsscpre  34891  dihord4  34915  dihord5apre  34919  dihmeetlem20N  34983  mapdh9a  35447
  Copyright terms: Public domain W3C validator