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  6063  omeu  6819  tsmsxp  18172  tgqioo  18819  ovolunlem2  19382  plyadd  20124  plymul  20125  coeeu  20132  ntrivcvgmul  25219  btwnconn1lem2  25970  btwnconn1lem3  25971  btwnconn1lem12  25980  pellex  26835  jm2.27  27016  athgt  30092  2llnjN  30203  4atlem12b  30247  lncmp  30419  cdlema2N  30428  cdlemc2  30828  cdleme5  30876  cdleme11a  30896  cdleme21ct  30965  cdleme21  30973  cdleme22eALTN  30981  cdleme24  30988  cdleme27cl  31002  cdleme27a  31003  cdleme28  31009  cdleme36a  31096  cdleme42b  31114  cdleme48fvg  31136  cdlemf  31199  cdlemk39  31552  cdlemkid1  31558  dihlsscpre  31871  dihord4  31895  dihord5apre  31899  dihmeetlem20N  31963  mapdh9a  32427
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