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

Theorem simp31l 1122
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 1023 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
213ad2ant3 1022 1  |-  ( ( ta  /\  et  /\  ( ( ph  /\  ps )  /\  ch  /\  th ) )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 976
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 187  df-an 371  df-3an 978
This theorem is referenced by:  ps-2c  32558  cdlema1N  32821  trlval3  33218  cdleme12  33302  cdlemednpq  33330  cdleme19d  33338  cdleme19e  33339  cdleme20f  33346  cdleme20h  33348  cdleme20l2  33353  cdleme20l  33354  cdleme20m  33355  cdleme21j  33368  cdleme22a  33372  cdleme22cN  33374  cdleme22f2  33379  cdleme32b  33474  cdlemg12f  33680  cdlemg12g  33681  cdlemg12  33682  cdlemg28a  33725  cdlemg31b0N  33726  cdlemg29  33737  cdlemg33a  33738  cdlemg36  33746  cdlemg42  33761  cdlemk16a  33888  cdlemk21-2N  33923  cdlemk32  33929  cdlemkid2  33956  cdlemk54  33990  cdlemk55a  33991  dihord10  34256
  Copyright terms: Public domain W3C validator