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

Theorem simpr1l 1014
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 981 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
21adantl 453 1  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )
)  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  oppccatid  13937  subccatid  14035  setccatid  14231  catccatid  14249  xpccatid  14277  dmdprdsplit  15597  neiptopnei  17188  neitr  17236  neitx  17631  tx1stc  17674  utop3cls  18273  metustsymOLD  18583  metustsym  18584  esumpcvgval  24460  ax5seg  25869  ifscgr  25970  brofs2  26003  brifs2  26004  btwnconn1lem8  26020  btwnconn1lem12  26024  seglecgr12im  26036  stoweidlem60  27776  frgrawopreg  28375  lhp2lt  30735  cdlemd1  30932  cdleme3b  30963  cdleme3c  30964  cdleme3e  30966  cdlemf2  31296  cdlemg4c  31346  cdlemn11pre  31945  dihmeetlem12N  32053
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