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  14780  subccatid  14878  setccatid  15074  catccatid  15092  xpccatid  15120  gsmsymgreqlem1  16057  dmdprdsplit  16671  neiptopnei  18871  neitr  18919  neitx  19315  tx1stc  19358  utop3cls  19961  metustsymOLD  20271  metustsym  20272  ax5seg  23356  esumpcvgval  26692  ifscgr  28239  brofs2  28272  brifs2  28273  btwnconn1lem8  28289  btwnconn1lem12  28293  seglecgr12im  28305  stoweidlem60  30023  frgrawopreg  30810  lhp2lt  34003  cdlemd1  34200  cdleme3b  34231  cdleme3c  34232  cdleme3e  34234  cdlemf2  34564  cdlemg4c  34614  cdlemn11pre  35213  dihmeetlem12N  35321
  Copyright terms: Public domain W3C validator