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

Theorem simpr1r 1015
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 982 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
21adantl 453 1  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )
)  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  oppccatid  13908  subccatid  14006  setccatid  14202  catccatid  14220  xpccatid  14248  dmdprdsplit  15568  neitr  17206  neitx  17600  tx1stc  17643  utop3cls  18242  metustsymOLD  18552  metustsym  18553  esumpcvgval  24429  ifscgr  25890  btwnconn1lem8  25940  btwnconn1lem11  25943  btwnconn1lem12  25944  segletr  25960  broutsideof3  25972  stoweidlem60  27684  frgrawopreg  28160  lhp2lt  30495  cdlemf2  31056  cdlemn11pre  31705
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator