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  13945  subccatid  14043  setccatid  14239  catccatid  14257  xpccatid  14285  dmdprdsplit  15605  neiptopnei  17196  neitr  17244  neitx  17639  tx1stc  17682  utop3cls  18281  metustsymOLD  18591  metustsym  18592  esumpcvgval  24468  ax5seg  25877  ifscgr  25978  brofs2  26011  brifs2  26012  btwnconn1lem8  26028  btwnconn1lem12  26032  seglecgr12im  26044  stoweidlem60  27785  frgrawopreg  28438  lhp2lt  30798  cdlemd1  30995  cdleme3b  31026  cdleme3c  31027  cdleme3e  31029  cdlemf2  31359  cdlemg4c  31409  cdlemn11pre  32008  dihmeetlem12N  32116
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