MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp32r Structured version   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  30515  paddasslem15  30558  4atex2-0aOLDN  30802  4atex3  30805  cdleme19b  31028  cdleme19d  31030  cdleme19e  31031  cdleme20d  31036  cdleme20f  31038  cdleme20g  31039  cdleme21d  31054  cdleme21e  31055  cdleme22cN  31066  cdleme22e  31068  cdleme22f2  31071  cdleme26e  31083  cdleme28a  31094  cdleme37m  31186  cdlemg28b  31427  cdlemk3  31557  cdlemk12  31574  cdlemk12u  31596  cdlemkoatnle-2N  31599  cdlemk13-2N  31600  cdlemkole-2N  31601  cdlemk14-2N  31602  cdlemk15-2N  31603  cdlemk16-2N  31604  cdlemk17-2N  31605  cdlemk18-2N  31610  cdlemk19-2N  31611  cdlemk7u-2N  31612  cdlemk11u-2N  31613  cdlemk20-2N  31616  cdlemk30  31618  cdlemk23-3  31626  cdlemk24-3  31627
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