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

Theorem simp1rr 1063
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 757 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ps )
213ad2ant1 1018 1  |-  ( ( ( ch  /\  ( ph  /\  ps ) )  /\  th  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 974
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 976
This theorem is referenced by:  f1imass  6157  smo11  7037  zsupss  11180  lsmcv  17661  lspsolvlem  17662  mat2pmatghm  19104  mat2pmatmul  19105  nrmr0reg  20123  plyadd  22487  plymul  22488  coeeu  22495  ax5seglem6  24109  archiabl  27615  sseqval  28200  wsuclem  29356  btwnconn1lem1  29712  btwnconn1lem2  29713  btwnconn1lem12  29723  pellex  30746  limcperiod  31542  lshpsmreu  34568  1cvratlt  34932  llnle  34976  lvolex3N  34996  lnjatN  35238  lncvrat  35240  lncmp  35241  cdlemd6  35662  cdlemk19ylem  36390
  Copyright terms: Public domain W3C validator