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

Theorem simpr1r 1014
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 981 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
21adantl 452 1  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )
)  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 935
This theorem is referenced by:  oppccatid  13832  subccatid  13930  setccatid  14126  catccatid  14144  xpccatid  14172  dmdprdsplit  15492  tx1stc  17561  metustsym  23798  esumpcvgval  23933  ifscgr  25409  btwnconn1lem8  25459  btwnconn1lem11  25462  btwnconn1lem12  25463  segletr  25479  broutsideof3  25491  stoweidlem60  27315  frgrawopreg  27884  lhp2lt  30261  cdlemf2  30822  cdlemn11pre  31471
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 937
  Copyright terms: Public domain W3C validator