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

Theorem simpr1l 1012
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpr1l  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )
)  ->  ph )

Proof of Theorem simpr1l
StepHypRef Expression
1 simp1l 979 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
21adantl 452 1  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )
)  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  oppccatid  13638  subccatid  13736  setccatid  13932  catccatid  13950  xpccatid  13978  dmdprdsplit  15298  tx1stc  17360  esumpcvgval  23461  ax5seg  24638  ifscgr  24739  brofs2  24772  brifs2  24773  btwnconn1lem8  24789  btwnconn1lem12  24793  seglecgr12im  24805  stoweidlem60  27912  lhp2lt  30812  cdlemd1  31009  cdleme3b  31040  cdleme3c  31041  cdleme3e  31043  cdlemf2  31373  cdlemg4c  31423  cdlemn11pre  32022  dihmeetlem12N  32130
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