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

Theorem simp3ll 1029
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 732 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )
213ad2ant3 981 1  |-  ( ( th  /\  ta  /\  ( ( ph  /\  ps )  /\  ch )
)  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  f1oiso2  6108  omeu  6864  tsmsxp  18222  tgqioo  18869  ovolunlem2  19432  plyadd  20174  plymul  20175  coeeu  20182  ntrivcvgmul  25265  btwnconn1lem2  26057  btwnconn1lem3  26058  btwnconn1lem12  26067  pellex  27010  jm2.27  27191  athgt  30427  2llnjN  30538  4atlem12b  30582  lncmp  30754  cdlema2N  30763  cdlemc2  31163  cdleme5  31211  cdleme11a  31231  cdleme21ct  31300  cdleme21  31308  cdleme22eALTN  31316  cdleme24  31323  cdleme27cl  31337  cdleme27a  31338  cdleme28  31344  cdleme36a  31431  cdleme42b  31449  cdleme48fvg  31471  cdlemf  31534  cdlemk39  31887  cdlemkid1  31893  dihlsscpre  32206  dihord4  32230  dihord5apre  32234  dihmeetlem20N  32298  mapdh9a  32762
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator