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

Theorem simp3ll 1067
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 1019 1  |-  ( ( th  /\  ta  /\  ( ( ph  /\  ps )  /\  ch )
)  ->  ph )
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  6237  omeu  7235  tsmsxp  20484  tgqioo  21132  ovolunlem2  21736  plyadd  22441  plymul  22442  coeeu  22449  tghilbert1_2  23829  ntrivcvgmul  28889  btwnconn1lem2  29591  btwnconn1lem3  29592  btwnconn1lem12  29601  pellex  30602  jm2.27  30781  athgt  34469  2llnjN  34580  4atlem12b  34624  lncmp  34796  cdlema2N  34805  cdlemc2  35205  cdleme5  35253  cdleme11a  35273  cdleme21ct  35342  cdleme21  35350  cdleme22eALTN  35358  cdleme24  35365  cdleme27cl  35379  cdleme27a  35380  cdleme28  35386  cdleme36a  35473  cdleme42b  35491  cdleme48fvg  35513  cdlemf  35576  cdlemk39  35929  cdlemkid1  35935  dihlsscpre  36248  dihord4  36272  dihord5apre  36276  dihmeetlem20N  36340  mapdh9a  36804
  Copyright terms: Public domain W3C validator