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  29090  cdlema1N  29353  cdlemednpq  29861  cdleme19e  29869  cdleme20h  29878  cdleme20j  29880  cdleme20l2  29883  cdleme20m  29885  cdleme22a  29902  cdleme22cN  29904  cdleme22f2  29909  cdleme26f2ALTN  29926  cdleme37m  30024  cdlemg12f  30210  cdlemg12g  30211  cdlemg12  30212  cdlemg28a  30255  cdlemg29  30267  cdlemg33a  30268  cdlemg36  30276  cdlemk16a  30418  cdlemk21-2N  30453  cdlemk54  30520  dihord10  30786
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