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

Theorem simp33r 1158
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp33r  |-  ( ( ta  /\  et  /\  ( ch  /\  th  /\  ( ph  /\  ps )
) )  ->  ps )

Proof of Theorem simp33r
StepHypRef Expression
1 simp3r 1059 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ps )
213ad2ant3 1053 1  |-  ( ( ta  /\  et  /\  ( ch  /\  th  /\  ( ph  /\  ps )
) )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    /\ w3a 1007
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 190  df-an 378  df-3an 1009
This theorem is referenced by:  totprob  29333  cdleme19b  33942  cdleme19e  33945  cdleme20h  33954  cdleme20l2  33959  cdleme20m  33961  cdleme21d  33968  cdleme21e  33969  cdleme22eALTN  33983  cdleme22f2  33985  cdleme22g  33986  cdleme26e  33997  cdleme37m  34100  cdlemeg46gfre  34170  cdlemg28a  34331  cdlemg28b  34341  cdlemk5a  34473  cdlemk6  34475
  Copyright terms: Public domain W3C validator