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

Theorem simp31r 1081
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 982 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
213ad2ant3 980 1  |-  ( ( ta  /\  et  /\  ( ( ph  /\  ps )  /\  ch  /\  th ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  ps-2c  30325  cdlema1N  30588  cdlemednpq  31096  cdleme19e  31104  cdleme20h  31113  cdleme20j  31115  cdleme20l2  31118  cdleme20m  31120  cdleme22a  31137  cdleme22cN  31139  cdleme22f2  31144  cdleme26f2ALTN  31161  cdleme37m  31259  cdlemg12f  31445  cdlemg12g  31446  cdlemg12  31447  cdlemg28a  31490  cdlemg29  31502  cdlemg33a  31503  cdlemg36  31511  cdlemk16a  31653  cdlemk21-2N  31688  cdlemk54  31755  dihord10  32021
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator