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

Theorem simp1rr 1071
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 764 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ps )
213ad2ant1 1026 1  |-  ( ( ( ch  /\  ( ph  /\  ps ) )  /\  th  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  f1imass  6124  smo11  7038  zsupss  11204  lsmcv  18307  lspsolvlem  18308  mat2pmatghm  19696  mat2pmatmul  19697  nrmr0reg  20706  plyadd  23113  plymul  23114  coeeu  23121  ax5seglem6  24906  archiabl  28466  mdetpmtr1  28601  sseqval  29173  wsuclem  30459  btwnconn1lem1  30803  btwnconn1lem2  30804  btwnconn1lem12  30814  lshpsmreu  32587  1cvratlt  32951  llnle  32995  lvolex3N  33015  lnjatN  33257  lncvrat  33259  lncmp  33260  cdlemd6  33681  cdlemk19ylem  34409  pellex  35592  limcperiod  37591
  Copyright terms: Public domain W3C validator