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

Theorem simp31l 1111
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp31l  |-  ( ( ta  /\  et  /\  ( ( ph  /\  ps )  /\  ch  /\  th ) )  ->  ph )

Proof of Theorem simp31l
StepHypRef Expression
1 simp1l 1012 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
213ad2ant3 1011 1  |-  ( ( ta  /\  et  /\  ( ( ph  /\  ps )  /\  ch  /\  th ) )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  ps-2c  33478  cdlema1N  33741  trlval3  34137  cdleme12  34221  cdlemednpq  34249  cdleme19d  34256  cdleme19e  34257  cdleme20f  34264  cdleme20h  34266  cdleme20l2  34271  cdleme20l  34272  cdleme20m  34273  cdleme21j  34286  cdleme22a  34290  cdleme22cN  34292  cdleme22f2  34297  cdleme32b  34392  cdlemg12f  34598  cdlemg12g  34599  cdlemg12  34600  cdlemg28a  34643  cdlemg31b0N  34644  cdlemg29  34655  cdlemg33a  34656  cdlemg36  34664  cdlemg42  34679  cdlemk16a  34806  cdlemk21-2N  34841  cdlemk32  34847  cdlemkid2  34874  cdlemk54  34908  cdlemk55a  34909  dihord10  35174
  Copyright terms: Public domain W3C validator