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

Theorem simpr1l 1015
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 982 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
21adantl 454 1  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )
)  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  oppccatid  13950  subccatid  14048  setccatid  14244  catccatid  14262  xpccatid  14290  dmdprdsplit  15610  neiptopnei  17201  neitr  17249  neitx  17644  tx1stc  17687  utop3cls  18286  metustsymOLD  18596  metustsym  18597  esumpcvgval  24473  ax5seg  25882  ifscgr  25983  brofs2  26016  brifs2  26017  btwnconn1lem8  26033  btwnconn1lem12  26037  seglecgr12im  26049  stoweidlem60  27799  frgrawopreg  28512  lhp2lt  30872  cdlemd1  31069  cdleme3b  31100  cdleme3c  31101  cdleme3e  31103  cdlemf2  31433  cdlemg4c  31483  cdlemn11pre  32082  dihmeetlem12N  32190
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator