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

Theorem simp31l 1080
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 981 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
213ad2ant3 980 1  |-  ( ( ta  /\  et  /\  ( ( ph  /\  ps )  /\  ch  /\  th ) )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  ps-2c  30325  cdlema1N  30588  trlval3  30984  cdleme12  31068  cdlemednpq  31096  cdleme19d  31103  cdleme19e  31104  cdleme20f  31111  cdleme20h  31113  cdleme20l2  31118  cdleme20l  31119  cdleme20m  31120  cdleme21j  31133  cdleme22a  31137  cdleme22cN  31139  cdleme22f2  31144  cdleme32b  31239  cdlemg12f  31445  cdlemg12g  31446  cdlemg12  31447  cdlemg28a  31490  cdlemg31b0N  31491  cdlemg29  31502  cdlemg33a  31503  cdlemg36  31511  cdlemg42  31526  cdlemk16a  31653  cdlemk21-2N  31688  cdlemk32  31694  cdlemkid2  31721  cdlemk54  31755  cdlemk55a  31756  dihord10  32021
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator