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

Theorem simpr2r 1017
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 984 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ps )
21adantl 453 1  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  th )
)  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  oppccatid  13945  subccatid  14043  setccatid  14239  catccatid  14257  xpccatid  14285  kerf1hrm  24262  ax5seg  25877  segconeq  25944  ifscgr  25978  brofs2  26011  brifs2  26012  idinside  26018  btwnconn1lem8  26028  btwnconn1lem11  26031  btwnconn1lem12  26032  segcon2  26039  seglecgr12im  26044  lplnexllnN  30361  paddasslem9  30625  paddasslem15  30631  pmodlem2  30644  lhp2lt  30798
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator