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

Theorem simpr1r 1013
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 980 . 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 934
This theorem is referenced by:  oppccatid  13622  subccatid  13720  setccatid  13916  catccatid  13934  xpccatid  13962  dmdprdsplit  15282  tx1stc  17344  esumpcvgval  23446  ifscgr  24667  btwnconn1lem8  24717  btwnconn1lem11  24720  btwnconn1lem12  24721  segletr  24737  broutsideof3  24749  stoweidlem60  27809  lhp2lt  30190  cdlemf2  30751  cdlemn11pre  31400
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 936
  Copyright terms: Public domain W3C validator