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

Theorem simpr1l 1052
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 1019 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
21adantl 466 1  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )
)  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 972
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 185  df-an 371  df-3an 974
This theorem is referenced by:  oppccatid  14988  subccatid  15086  setccatid  15282  catccatid  15300  xpccatid  15328  gsmsymgreqlem1  16326  dmdprdsplit  16967  neiptopnei  19503  neitr  19551  neitx  19978  tx1stc  20021  utop3cls  20624  metustsymOLD  20934  metustsym  20935  ax5seg  24110  frgrawopreg  24918  esumpcvgval  27954  ifscgr  29666  brofs2  29699  brifs2  29700  btwnconn1lem8  29716  btwnconn1lem12  29720  seglecgr12im  29732  stoweidlem60  31731  estrccatid  32484  lhp2lt  35448  cdlemd1  35646  cdleme3b  35677  cdleme3c  35678  cdleme3e  35680  cdlemf2  36011  cdlemg4c  36061  cdlemn11pre  36660  dihmeetlem12N  36768
  Copyright terms: Public domain W3C validator