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

Theorem simp1rr 1021
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 733 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ps )
213ad2ant1 976 1  |-  ( ( ( ch  /\  ( ph  /\  ps ) )  /\  th  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  f1imass  5830  smo11  6423  zsupss  10354  lsmcv  15943  lspsolvlem  15944  nrmr0reg  17496  plyadd  19652  plymul  19653  coeeu  19660  ax5seglem6  24948  btwnconn1lem1  25096  btwnconn1lem2  25097  btwnconn1lem12  25107  pellex  26068  lshpsmreu  29117  1cvratlt  29481  llnle  29525  lvolex3N  29545  lnjatN  29787  lncvrat  29789  lncmp  29790  cdlemd6  30210  cdlemk19ylem  30937
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator