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

Theorem simpr1l 1045
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 1012 . 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 965
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 967
This theorem is referenced by:  oppccatid  14650  subccatid  14748  setccatid  14944  catccatid  14962  xpccatid  14990  gsmsymgreqlem1  15926  dmdprdsplit  16534  neiptopnei  18711  neitr  18759  neitx  19155  tx1stc  19198  utop3cls  19801  metustsymOLD  20111  metustsym  20112  ax5seg  23135  esumpcvgval  26479  ifscgr  28026  brofs2  28059  brifs2  28060  btwnconn1lem8  28076  btwnconn1lem12  28080  seglecgr12im  28092  stoweidlem60  29808  frgrawopreg  30595  lhp2lt  33485  cdlemd1  33682  cdleme3b  33713  cdleme3c  33714  cdleme3e  33716  cdlemf2  34046  cdlemg4c  34096  cdlemn11pre  34695  dihmeetlem12N  34803
  Copyright terms: Public domain W3C validator