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  6012  omeu  6765  tsmsxp  18106  tgqioo  18703  ovolunlem2  19262  plyadd  20004  plymul  20005  coeeu  20012  ntrivcvgmul  25010  btwnconn1lem2  25737  btwnconn1lem3  25738  btwnconn1lem12  25747  pellex  26590  jm2.27  26771  athgt  29571  2llnjN  29682  4atlem12b  29726  lncmp  29898  cdlema2N  29907  cdlemc2  30307  cdleme5  30355  cdleme11a  30375  cdleme21ct  30444  cdleme21  30452  cdleme22eALTN  30460  cdleme24  30467  cdleme27cl  30481  cdleme27a  30482  cdleme28  30488  cdleme36a  30575  cdleme42b  30593  cdleme48fvg  30615  cdlemf  30678  cdlemk39  31031  cdlemkid1  31037  dihlsscpre  31350  dihord4  31374  dihord5apre  31378  dihmeetlem20N  31442  mapdh9a  31906
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