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  13622  subccatid  13720  setccatid  13916  catccatid  13934  xpccatid  13962  ax5seg  24566  segconeq  24633  ifscgr  24667  brofs2  24700  brifs2  24701  idinside  24707  btwnconn1lem8  24717  btwnconn1lem11  24720  btwnconn1lem12  24721  segcon2  24728  seglecgr12im  24733  codsubc  25853  lplnexllnN  29753  paddasslem9  30017  paddasslem15  30023  pmodlem2  30036  lhp2lt  30190
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