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

Theorem simpr2r 1048
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 1015 . 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 965
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 967
This theorem is referenced by:  oppccatid  14772  subccatid  14870  setccatid  15066  catccatid  15084  xpccatid  15112  gsmsymgreqlem1  16049  kerf1hrm  16949  ax5seg  23331  segconeq  28180  ifscgr  28214  brofs2  28247  brifs2  28248  idinside  28254  btwnconn1lem8  28264  btwnconn1lem11  28267  btwnconn1lem12  28268  segcon2  28275  seglecgr12im  28280  lplnexllnN  33527  paddasslem9  33791  paddasslem15  33797  pmodlem2  33810  lhp2lt  33964
  Copyright terms: Public domain W3C validator