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

Theorem simpr1l 1053
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 1020 . 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 973
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 975
This theorem is referenced by:  oppccatid  14992  subccatid  15090  setccatid  15286  catccatid  15304  xpccatid  15332  gsmsymgreqlem1  16327  dmdprdsplit  16968  neiptopnei  19501  neitr  19549  neitx  19976  tx1stc  20019  utop3cls  20622  metustsymOLD  20932  metustsym  20933  ax5seg  24064  frgrawopreg  24873  esumpcvgval  27909  ifscgr  29621  brofs2  29654  brifs2  29655  btwnconn1lem8  29671  btwnconn1lem12  29675  seglecgr12im  29687  stoweidlem60  31683  lhp2lt  35198  cdlemd1  35395  cdleme3b  35426  cdleme3c  35427  cdleme3e  35429  cdlemf2  35759  cdlemg4c  35809  cdlemn11pre  36408  dihmeetlem12N  36516
  Copyright terms: Public domain W3C validator