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

Theorem simp32l 1082
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 983 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
213ad2ant3 980 1  |-  ( ( ta  /\  et  /\  ( ch  /\  ( ph  /\  ps )  /\  th ) )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  cdlema1N  30588  paddasslem15  30631  4atex2-0aOLDN  30875  4atex3  30878  trlval3  30984  cdleme12  31068  cdleme19b  31101  cdleme19d  31103  cdleme19e  31104  cdleme20d  31109  cdleme20f  31111  cdleme20g  31112  cdleme21d  31127  cdleme21e  31128  cdleme21f  31129  cdleme22cN  31139  cdleme22e  31141  cdleme22f2  31144  cdleme22g  31145  cdleme26e  31156  cdleme28a  31167  cdleme37m  31259  cdleme39n  31263  cdlemg28b  31500  cdlemk3  31630  cdlemk12  31647  cdlemk12u  31669  cdlemkoatnle-2N  31672  cdlemk13-2N  31673  cdlemkole-2N  31674  cdlemk14-2N  31675  cdlemk15-2N  31676  cdlemk16-2N  31677  cdlemk17-2N  31678  cdlemk18-2N  31683  cdlemk19-2N  31684  cdlemk7u-2N  31685  cdlemk11u-2N  31686  cdlemk20-2N  31689  cdlemk30  31691  cdlemk23-3  31699  cdlemk24-3  31700
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