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

Theorem simp31r 1079
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 980 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
213ad2ant3 978 1  |-  ( ( ta  /\  et  /\  ( ( ph  /\  ps )  /\  ch  /\  th ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  ps-2c  30339  cdlema1N  30602  cdlemednpq  31110  cdleme19e  31118  cdleme20h  31127  cdleme20j  31129  cdleme20l2  31132  cdleme20m  31134  cdleme22a  31151  cdleme22cN  31153  cdleme22f2  31158  cdleme26f2ALTN  31175  cdleme37m  31273  cdlemg12f  31459  cdlemg12g  31460  cdlemg12  31461  cdlemg28a  31504  cdlemg29  31516  cdlemg33a  31517  cdlemg36  31525  cdlemk16a  31667  cdlemk21-2N  31702  cdlemk54  31769  dihord10  32035
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator