MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp31r 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  30010  cdlema1N  30273  cdlemednpq  30781  cdleme19e  30789  cdleme20h  30798  cdleme20j  30800  cdleme20l2  30803  cdleme20m  30805  cdleme22a  30822  cdleme22cN  30824  cdleme22f2  30829  cdleme26f2ALTN  30846  cdleme37m  30944  cdlemg12f  31130  cdlemg12g  31131  cdlemg12  31132  cdlemg28a  31175  cdlemg29  31187  cdlemg33a  31188  cdlemg36  31196  cdlemk16a  31338  cdlemk21-2N  31373  cdlemk54  31440  dihord10  31706
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