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

Theorem simp31r 1112
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 1013 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
213ad2ant3 1011 1  |-  ( ( ta  /\  et  /\  ( ( ph  /\  ps )  /\  ch  /\  th ) )  ->  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:  ps-2c  33454  cdlema1N  33717  cdlemednpq  34225  cdleme19e  34233  cdleme20h  34242  cdleme20j  34244  cdleme20l2  34247  cdleme20m  34249  cdleme22a  34266  cdleme22cN  34268  cdleme22f2  34273  cdleme26f2ALTN  34290  cdleme37m  34388  cdlemg12f  34574  cdlemg12g  34575  cdlemg12  34576  cdlemg28a  34619  cdlemg29  34631  cdlemg33a  34632  cdlemg36  34640  cdlemk16a  34782  cdlemk21-2N  34817  cdlemk54  34884  dihord10  35150
  Copyright terms: Public domain W3C validator