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

Theorem simpr2r 1055
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 1022 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ps )
21adantl 466 1  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  th )
)  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 972
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 371  df-3an 974
This theorem is referenced by:  oppccatid  14986  subccatid  15084  setccatid  15280  catccatid  15298  xpccatid  15326  gsmsymgreqlem1  16324  kerf1hrm  17260  ax5seg  24106  segconeq  29628  ifscgr  29662  brofs2  29695  brifs2  29696  idinside  29702  btwnconn1lem8  29712  btwnconn1lem11  29715  btwnconn1lem12  29716  segcon2  29723  seglecgr12im  29728  estrccatid  32476  lplnexllnN  34990  paddasslem9  35254  paddasslem15  35260  pmodlem2  35273  lhp2lt  35427
  Copyright terms: Public domain W3C validator