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

Theorem simp31r 1120
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 1021 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
213ad2ant3 1019 1  |-  ( ( ta  /\  et  /\  ( ( ph  /\  ps )  /\  ch  /\  th ) )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 975
This theorem is referenced by:  ps-2c  34324  cdlema1N  34587  cdlemednpq  35095  cdleme19e  35103  cdleme20h  35112  cdleme20j  35114  cdleme20l2  35117  cdleme20m  35119  cdleme22a  35136  cdleme22cN  35138  cdleme22f2  35143  cdleme26f2ALTN  35160  cdleme37m  35258  cdlemg12f  35444  cdlemg12g  35445  cdlemg12  35446  cdlemg28a  35489  cdlemg29  35501  cdlemg33a  35502  cdlemg36  35510  cdlemk16a  35652  cdlemk21-2N  35687  cdlemk54  35754  dihord10  36020
  Copyright terms: Public domain W3C validator