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

Theorem simpr1r 1046
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpr1r  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )
)  ->  ps )

Proof of Theorem simpr1r
StepHypRef Expression
1 simp1r 1013 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
21adantl 466 1  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )
)  ->  ps )
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  14663  subccatid  14761  setccatid  14957  catccatid  14975  xpccatid  15003  gsmsymgreqlem1  15940  dmdprdsplit  16551  neitr  18789  neitx  19185  tx1stc  19228  utop3cls  19831  metustsymOLD  20141  metustsym  20142  archiabllem1  26215  esumpcvgval  26532  ifscgr  28080  btwnconn1lem8  28130  btwnconn1lem11  28133  btwnconn1lem12  28134  segletr  28150  broutsideof3  28162  stoweidlem60  29860  frgrawopreg  30647  lhp2lt  33650  cdlemf2  34211  cdlemn11pre  34860
  Copyright terms: Public domain W3C validator