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

Theorem simp31r 1130
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 1031 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
213ad2ant3 1029 1  |-  ( ( ta  /\  et  /\  ( ( ph  /\  ps )  /\  ch  /\  th ) )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 983
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 189  df-an 373  df-3an 985
This theorem is referenced by:  ps-2c  33018  cdlema1N  33281  cdlemednpq  33790  cdleme19e  33799  cdleme20h  33808  cdleme20j  33810  cdleme20l2  33813  cdleme20m  33815  cdleme22a  33832  cdleme22cN  33834  cdleme22f2  33839  cdleme26f2ALTN  33856  cdleme37m  33954  cdlemg12f  34140  cdlemg12g  34141  cdlemg12  34142  cdlemg28a  34185  cdlemg29  34197  cdlemg33a  34198  cdlemg36  34206  cdlemk16a  34348  cdlemk21-2N  34383  cdlemk54  34450  dihord10  34716
  Copyright terms: Public domain W3C validator