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

Theorem simp31r 1123
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp31r  |-  ( ( ta  /\  et  /\  ( ( ph  /\  ps )  /\  ch  /\  th ) )  ->  ps )

Proof of Theorem simp31r
StepHypRef Expression
1 simp1r 1024 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
213ad2ant3 1022 1  |-  ( ( ta  /\  et  /\  ( ( ph  /\  ps )  /\  ch  /\  th ) )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 976
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 187  df-an 371  df-3an 978
This theorem is referenced by:  ps-2c  32558  cdlema1N  32821  cdlemednpq  33330  cdleme19e  33339  cdleme20h  33348  cdleme20j  33350  cdleme20l2  33353  cdleme20m  33355  cdleme22a  33372  cdleme22cN  33374  cdleme22f2  33379  cdleme26f2ALTN  33396  cdleme37m  33494  cdlemg12f  33680  cdlemg12g  33681  cdlemg12  33682  cdlemg28a  33725  cdlemg29  33737  cdlemg33a  33738  cdlemg36  33746  cdlemk16a  33888  cdlemk21-2N  33923  cdlemk54  33990  dihord10  34256
  Copyright terms: Public domain W3C validator