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

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

Proof of Theorem simp32r
StepHypRef Expression
1 simp2r 984 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ps )
213ad2ant3 980 1  |-  ( ( ta  /\  et  /\  ( ch  /\  ( ph  /\  ps )  /\  th ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  cdlema1N  29905  paddasslem15  29948  4atex2-0aOLDN  30192  4atex3  30195  cdleme19b  30418  cdleme19d  30420  cdleme19e  30421  cdleme20d  30426  cdleme20f  30428  cdleme20g  30429  cdleme21d  30444  cdleme21e  30445  cdleme22cN  30456  cdleme22e  30458  cdleme22f2  30461  cdleme26e  30473  cdleme28a  30484  cdleme37m  30576  cdlemg28b  30817  cdlemk3  30947  cdlemk12  30964  cdlemk12u  30986  cdlemkoatnle-2N  30989  cdlemk13-2N  30990  cdlemkole-2N  30991  cdlemk14-2N  30992  cdlemk15-2N  30993  cdlemk16-2N  30994  cdlemk17-2N  30995  cdlemk18-2N  31000  cdlemk19-2N  31001  cdlemk7u-2N  31002  cdlemk11u-2N  31003  cdlemk20-2N  31006  cdlemk30  31008  cdlemk23-3  31016  cdlemk24-3  31017
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