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

Theorem simp3ll 1026
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 730 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )
213ad2ant3 978 1  |-  ( ( th  /\  ta  /\  ( ( ph  /\  ps )  /\  ch )
)  ->  ph )
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  btwnconn1lem12  24721  pellex  26920  jm2.27  27101  athgt  29645  2llnjN  29756  4atlem12b  29800  lncmp  29972  cdlema2N  29981  cdlemc2  30381  cdleme5  30429  cdleme11a  30449  cdleme21ct  30518  cdleme21  30526  cdleme22eALTN  30534  cdleme24  30541  cdleme27cl  30555  cdleme27a  30556  cdleme28  30562  cdleme36a  30649  cdleme42b  30667  cdleme48fvg  30689  cdlemf  30752  cdlemk39  31105  cdlemkid1  31111  dihlsscpre  31424  dihord4  31448  dihord5apre  31452  dihmeetlem20N  31516  mapdh9a  31980
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