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

Theorem simp32r 1122
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 1023 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ps )
213ad2ant3 1019 1  |-  ( ( ta  /\  et  /\  ( ch  /\  ( ph  /\  ps )  /\  th ) )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  cdlema1N  34605  paddasslem15  34648  4atex2-0aOLDN  34892  4atex3  34895  cdleme19b  35118  cdleme19d  35120  cdleme19e  35121  cdleme20d  35126  cdleme20f  35128  cdleme20g  35129  cdleme21d  35144  cdleme21e  35145  cdleme22cN  35156  cdleme22e  35158  cdleme22f2  35161  cdleme26e  35173  cdleme28a  35184  cdleme37m  35276  cdlemg28b  35517  cdlemk3  35647  cdlemk12  35664  cdlemk12u  35686  cdlemkoatnle-2N  35689  cdlemk13-2N  35690  cdlemkole-2N  35691  cdlemk14-2N  35692  cdlemk15-2N  35693  cdlemk16-2N  35694  cdlemk17-2N  35695  cdlemk18-2N  35700  cdlemk19-2N  35701  cdlemk7u-2N  35702  cdlemk11u-2N  35703  cdlemk20-2N  35706  cdlemk30  35708  cdlemk23-3  35716  cdlemk24-3  35717
  Copyright terms: Public domain W3C validator