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

Theorem simpr1r 1016
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 983 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
21adantl 454 1  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )
)  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  oppccatid  13950  subccatid  14048  setccatid  14244  catccatid  14262  xpccatid  14290  dmdprdsplit  15610  neitr  17249  neitx  17644  tx1stc  17687  utop3cls  18286  metustsymOLD  18596  metustsym  18597  esumpcvgval  24473  ifscgr  25983  btwnconn1lem8  26033  btwnconn1lem11  26036  btwnconn1lem12  26037  segletr  26053  broutsideof3  26065  stoweidlem60  27799  frgrawopreg  28512  lhp2lt  30872  cdlemf2  31433  cdlemn11pre  32082
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator