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

Theorem simpr2r 1054
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 1021 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ps )
21adantl 464 1  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  th )
)  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 973
This theorem is referenced by:  oppccatid  15210  subccatid  15337  setccatid  15565  catccatid  15583  estrccatid  15603  xpccatid  15659  gsmsymgreqlem1  16657  kerf1hrm  17590  ax5seg  24446  segconeq  29891  ifscgr  29925  brofs2  29958  brifs2  29959  idinside  29965  btwnconn1lem8  29975  btwnconn1lem11  29978  btwnconn1lem12  29979  segcon2  29986  seglecgr12im  29991  lplnexllnN  35704  paddasslem9  35968  paddasslem15  35974  pmodlem2  35987  lhp2lt  36141
  Copyright terms: Public domain W3C validator