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

Theorem simp32r 1081
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 982 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ps )
213ad2ant3 978 1  |-  ( ( ta  /\  et  /\  ( ch  /\  ( ph  /\  ps )  /\  th ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  cdlema1N  30602  paddasslem15  30645  4atex2-0aOLDN  30889  4atex3  30892  cdleme19b  31115  cdleme19d  31117  cdleme19e  31118  cdleme20d  31123  cdleme20f  31125  cdleme20g  31126  cdleme21d  31141  cdleme21e  31142  cdleme22cN  31153  cdleme22e  31155  cdleme22f2  31158  cdleme26e  31170  cdleme28a  31181  cdleme37m  31273  cdlemg28b  31514  cdlemk3  31644  cdlemk12  31661  cdlemk12u  31683  cdlemkoatnle-2N  31686  cdlemk13-2N  31687  cdlemkole-2N  31688  cdlemk14-2N  31689  cdlemk15-2N  31690  cdlemk16-2N  31691  cdlemk17-2N  31692  cdlemk18-2N  31697  cdlemk19-2N  31698  cdlemk7u-2N  31699  cdlemk11u-2N  31700  cdlemk20-2N  31703  cdlemk30  31705  cdlemk23-3  31713  cdlemk24-3  31714
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