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

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

Proof of Theorem simp32l
StepHypRef Expression
1 simp2l 1056 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
213ad2ant3 1053 1  |-  ( ( ta  /\  et  /\  ( ch  /\  ( ph  /\  ps )  /\  th ) )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    /\ w3a 1007
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 190  df-an 378  df-3an 1009
This theorem is referenced by:  cdlema1N  33427  paddasslem15  33470  4atex2-0aOLDN  33714  4atex3  33717  trlval3  33824  cdleme12  33908  cdleme19b  33942  cdleme19d  33944  cdleme19e  33945  cdleme20d  33950  cdleme20f  33952  cdleme20g  33953  cdleme21d  33968  cdleme21e  33969  cdleme21f  33970  cdleme22cN  33980  cdleme22e  33982  cdleme22f2  33985  cdleme22g  33986  cdleme26e  33997  cdleme28a  34008  cdleme37m  34100  cdleme39n  34104  cdlemg28b  34341  cdlemk3  34471  cdlemk12  34488  cdlemk12u  34510  cdlemkoatnle-2N  34513  cdlemk13-2N  34514  cdlemkole-2N  34515  cdlemk14-2N  34516  cdlemk15-2N  34517  cdlemk16-2N  34518  cdlemk17-2N  34519  cdlemk18-2N  34524  cdlemk19-2N  34525  cdlemk7u-2N  34526  cdlemk11u-2N  34527  cdlemk20-2N  34530  cdlemk30  34532  cdlemk23-3  34540  cdlemk24-3  34541
  Copyright terms: Public domain W3C validator