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  5788  smo11  6381  zsupss  10307  lsmcv  15894  lspsolvlem  15895  nrmr0reg  17440  plyadd  19599  plymul  19600  coeeu  19607  ax5seglem6  24562  btwnconn1lem1  24710  btwnconn1lem2  24711  btwnconn1lem12  24721  lppotos  26144  pellex  26920  lshpsmreu  29299  1cvratlt  29663  llnle  29707  lvolex3N  29727  lnjatN  29969  lncvrat  29971  lncmp  29972  cdlemd6  30392  cdlemk19ylem  31119
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