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  30273  paddasslem15  30316  4atex2-0aOLDN  30560  4atex3  30563  cdleme19b  30786  cdleme19d  30788  cdleme19e  30789  cdleme20d  30794  cdleme20f  30796  cdleme20g  30797  cdleme21d  30812  cdleme21e  30813  cdleme22cN  30824  cdleme22e  30826  cdleme22f2  30829  cdleme26e  30841  cdleme28a  30852  cdleme37m  30944  cdlemg28b  31185  cdlemk3  31315  cdlemk12  31332  cdlemk12u  31354  cdlemkoatnle-2N  31357  cdlemk13-2N  31358  cdlemkole-2N  31359  cdlemk14-2N  31360  cdlemk15-2N  31361  cdlemk16-2N  31362  cdlemk17-2N  31363  cdlemk18-2N  31368  cdlemk19-2N  31369  cdlemk7u-2N  31370  cdlemk11u-2N  31371  cdlemk20-2N  31374  cdlemk30  31376  cdlemk23-3  31384  cdlemk24-3  31385
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