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

Theorem simp3ll 1028
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 731 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )
213ad2ant3 980 1  |-  ( ( th  /\  ta  /\  ( ( ph  /\  ps )  /\  ch )
)  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  f1oiso2  6039  omeu  6795  tsmsxp  18145  tgqioo  18792  ovolunlem2  19355  plyadd  20097  plymul  20098  coeeu  20105  ntrivcvgmul  25191  btwnconn1lem2  25934  btwnconn1lem3  25935  btwnconn1lem12  25944  pellex  26796  jm2.27  26977  athgt  29950  2llnjN  30061  4atlem12b  30105  lncmp  30277  cdlema2N  30286  cdlemc2  30686  cdleme5  30734  cdleme11a  30754  cdleme21ct  30823  cdleme21  30831  cdleme22eALTN  30839  cdleme24  30846  cdleme27cl  30860  cdleme27a  30861  cdleme28  30867  cdleme36a  30954  cdleme42b  30972  cdleme48fvg  30994  cdlemf  31057  cdlemk39  31410  cdlemkid1  31416  dihlsscpre  31729  dihord4  31753  dihord5apre  31757  dihmeetlem20N  31821  mapdh9a  32285
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator