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  13622  subccatid  13720  setccatid  13916  catccatid  13934  xpccatid  13962  dmdprdsplit  15282  tx1stc  17344  esumpcvgval  23446  ax5seg  24566  ifscgr  24667  brofs2  24700  brifs2  24701  btwnconn1lem8  24717  btwnconn1lem12  24721  seglecgr12im  24733  stoweidlem60  27809  lhp2lt  30190  cdlemd1  30387  cdleme3b  30418  cdleme3c  30419  cdleme3e  30421  cdlemf2  30751  cdlemg4c  30801  cdlemn11pre  31400  dihmeetlem12N  31508
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