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

Theorem simp32l 1080
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 981 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
213ad2ant3 978 1  |-  ( ( ta  /\  et  /\  ( ch  /\  ( ph  /\  ps )  /\  th ) )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  cdlema1N  29980  paddasslem15  30023  4atex2-0aOLDN  30267  4atex3  30270  trlval3  30376  cdleme12  30460  cdleme19b  30493  cdleme19d  30495  cdleme19e  30496  cdleme20d  30501  cdleme20f  30503  cdleme20g  30504  cdleme21d  30519  cdleme21e  30520  cdleme21f  30521  cdleme22cN  30531  cdleme22e  30533  cdleme22f2  30536  cdleme22g  30537  cdleme26e  30548  cdleme28a  30559  cdleme37m  30651  cdleme39n  30655  cdlemg28b  30892  cdlemk3  31022  cdlemk12  31039  cdlemk12u  31061  cdlemkoatnle-2N  31064  cdlemk13-2N  31065  cdlemkole-2N  31066  cdlemk14-2N  31067  cdlemk15-2N  31068  cdlemk16-2N  31069  cdlemk17-2N  31070  cdlemk18-2N  31075  cdlemk19-2N  31076  cdlemk7u-2N  31077  cdlemk11u-2N  31078  cdlemk20-2N  31081  cdlemk30  31083  cdlemk23-3  31091  cdlemk24-3  31092
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator