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

Theorem simp31l 1129
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 1030 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
213ad2ant3 1029 1  |-  ( ( ta  /\  et  /\  ( ( ph  /\  ps )  /\  ch  /\  th ) )  ->  ph )
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  trlval3  33678  cdleme12  33762  cdlemednpq  33790  cdleme19d  33798  cdleme19e  33799  cdleme20f  33806  cdleme20h  33808  cdleme20l2  33813  cdleme20l  33814  cdleme20m  33815  cdleme21j  33828  cdleme22a  33832  cdleme22cN  33834  cdleme22f2  33839  cdleme32b  33934  cdlemg12f  34140  cdlemg12g  34141  cdlemg12  34142  cdlemg28a  34185  cdlemg31b0N  34186  cdlemg29  34197  cdlemg33a  34198  cdlemg36  34206  cdlemg42  34221  cdlemk16a  34348  cdlemk21-2N  34383  cdlemk32  34389  cdlemkid2  34416  cdlemk54  34450  cdlemk55a  34451  dihord10  34716
  Copyright terms: Public domain W3C validator