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

Theorem simp32r 1131
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 1032 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ps )
213ad2ant3 1028 1  |-  ( ( ta  /\  et  /\  ( ch  /\  ( ph  /\  ps )  /\  th ) )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984
This theorem is referenced by:  cdlema1N  33065  paddasslem15  33108  4atex2-0aOLDN  33352  4atex3  33355  cdleme19b  33580  cdleme19d  33582  cdleme19e  33583  cdleme20d  33588  cdleme20f  33590  cdleme20g  33591  cdleme21d  33606  cdleme21e  33607  cdleme22cN  33618  cdleme22e  33620  cdleme22f2  33623  cdleme26e  33635  cdleme28a  33646  cdleme37m  33738  cdlemg28b  33979  cdlemk3  34109  cdlemk12  34126  cdlemk12u  34148  cdlemkoatnle-2N  34151  cdlemk13-2N  34152  cdlemkole-2N  34153  cdlemk14-2N  34154  cdlemk15-2N  34155  cdlemk16-2N  34156  cdlemk17-2N  34157  cdlemk18-2N  34162  cdlemk19-2N  34163  cdlemk7u-2N  34164  cdlemk11u-2N  34165  cdlemk20-2N  34168  cdlemk30  34170  cdlemk23-3  34178  cdlemk24-3  34179
  Copyright terms: Public domain W3C validator