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

Theorem simpr2r 1015
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpr2r  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  th )
)  ->  ps )

Proof of Theorem simpr2r
StepHypRef Expression
1 simp2r 982 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ps )
21adantl 452 1  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  th )
)  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  oppccatid  13638  subccatid  13736  setccatid  13932  catccatid  13950  xpccatid  13978  ax5seg  24638  segconeq  24705  ifscgr  24739  brofs2  24772  brifs2  24773  idinside  24779  btwnconn1lem8  24789  btwnconn1lem11  24792  btwnconn1lem12  24793  segcon2  24800  seglecgr12im  24805  codsubc  25956  lplnexllnN  30375  paddasslem9  30639  paddasslem15  30645  pmodlem2  30658  lhp2lt  30812
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