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

Theorem simpr1r 1054
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 1021 . 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 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  14975  subccatid  15073  setccatid  15269  catccatid  15287  xpccatid  15315  gsmsymgreqlem1  16260  dmdprdsplit  16898  neitr  19475  neitx  19871  tx1stc  19914  utop3cls  20517  metustsymOLD  20827  metustsym  20828  frgrawopreg  24754  archiabllem1  27427  esumpcvgval  27752  ifscgr  29299  btwnconn1lem8  29349  btwnconn1lem11  29352  btwnconn1lem12  29353  segletr  29369  broutsideof3  29381  stoweidlem60  31388  lhp2lt  34815  cdlemf2  35376  cdlemn11pre  36025
  Copyright terms: Public domain W3C validator