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

Theorem simp1rr 1054
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 756 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ps )
213ad2ant1 1009 1  |-  ( ( ( ch  /\  ( ph  /\  ps ) )  /\  th  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  f1imass  6079  smo11  6928  zsupss  11048  lsmcv  17337  lspsolvlem  17338  nrmr0reg  19447  plyadd  21811  plymul  21812  coeeu  21819  ax5seglem6  23325  archiabl  26353  sseqval  26908  wsuclem  27899  btwnconn1lem1  28255  btwnconn1lem2  28256  btwnconn1lem12  28266  pellex  29317  mat2pmatghm  31196  mat2pmatmul  31197  lshpsmreu  33063  1cvratlt  33427  llnle  33471  lvolex3N  33491  lnjatN  33733  lncvrat  33735  lncmp  33736  cdlemd6  34156  cdlemk19ylem  34883
  Copyright terms: Public domain W3C validator