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

Theorem simpr1r 1055
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 1022 . 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 974
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 976
This theorem is referenced by:  oppccatid  15096  subccatid  15194  setccatid  15390  catccatid  15408  xpccatid  15436  gsmsymgreqlem1  16434  dmdprdsplit  17075  neitr  19659  neitx  20086  tx1stc  20129  utop3cls  20732  metustsymOLD  21042  metustsym  21043  frgrawopreg  25027  archiabllem1  27715  esumpcvgval  28062  ifscgr  29670  btwnconn1lem8  29720  btwnconn1lem11  29723  btwnconn1lem12  29724  segletr  29740  broutsideof3  29752  stoweidlem60  31796  estrccatid  32604  lhp2lt  35600  cdlemf2  36163  cdlemn11pre  36812
  Copyright terms: Public domain W3C validator