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

Theorem simp3ll 1027
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 979 1  |-  ( ( th  /\  ta  /\  ( ( ph  /\  ps )  /\  ch )
)  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 935
This theorem is referenced by:  f1oiso2  5972  omeu  6725  tsmsxp  18050  tgqioo  18519  ovolunlem2  19072  plyadd  19814  plymul  19815  coeeu  19822  ntrivcvgmul  24799  btwnconn1lem2  25538  btwnconn1lem3  25539  btwnconn1lem12  25548  pellex  26511  jm2.27  26692  athgt  29704  2llnjN  29815  4atlem12b  29859  lncmp  30031  cdlema2N  30040  cdlemc2  30440  cdleme5  30488  cdleme11a  30508  cdleme21ct  30577  cdleme21  30585  cdleme22eALTN  30593  cdleme24  30600  cdleme27cl  30614  cdleme27a  30615  cdleme28  30621  cdleme36a  30708  cdleme42b  30726  cdleme48fvg  30748  cdlemf  30811  cdlemk39  31164  cdlemkid1  31170  dihlsscpre  31483  dihord4  31507  dihord5apre  31511  dihmeetlem20N  31575  mapdh9a  32039
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 937
  Copyright terms: Public domain W3C validator