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

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

Proof of Theorem simp33l
StepHypRef Expression
1 simp3l 1058 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
213ad2ant3 1053 1  |-  ( ( ta  /\  et  /\  ( ch  /\  th  /\  ( ph  /\  ps )
) )  ->  ph )
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  cdleme19d  33944  cdleme19e  33945  cdleme20h  33954  cdleme20l2  33959  cdleme20m  33961  cdleme21d  33968  cdleme21e  33969  cdleme22e  33982  cdleme22f2  33985  cdleme22g  33986  cdleme26e  33997  cdleme28a  34008  cdleme28b  34009  cdleme37m  34100  cdleme39n  34104  cdlemeg46gfre  34170  cdlemg28a  34331  cdlemg28b  34341  cdlemk3  34471  cdlemk5a  34473  cdlemk6  34475  cdlemkuat  34504  cdlemkid2  34562
  Copyright terms: Public domain W3C validator