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

Theorem simp1rr 1024
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp1rr  |-  ( ( ( ch  /\  ( ph  /\  ps ) )  /\  th  /\  ta )  ->  ps )

Proof of Theorem simp1rr
StepHypRef Expression
1 simprr 735 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ps )
213ad2ant1 979 1  |-  ( ( ( ch  /\  ( ph  /\  ps ) )  /\  th  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  f1imass  6011  smo11  6627  zsupss  10566  lsmcv  16214  lspsolvlem  16215  nrmr0reg  17782  plyadd  20137  plymul  20138  coeeu  20145  wsuclem  25577  ax5seglem6  25874  btwnconn1lem1  26022  btwnconn1lem2  26023  btwnconn1lem12  26033  pellex  26899  lshpsmreu  29908  1cvratlt  30272  llnle  30316  lvolex3N  30336  lnjatN  30578  lncvrat  30580  lncmp  30581  cdlemd6  31001  cdlemk19ylem  31728
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator