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

Theorem simp33l 1084
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 985 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
213ad2ant3 980 1  |-  ( ( ta  /\  et  /\  ( ch  /\  th  /\  ( ph  /\  ps )
) )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  totprob  24685  cdleme19b  31101  cdleme19d  31103  cdleme19e  31104  cdleme20h  31113  cdleme20l2  31118  cdleme20m  31120  cdleme21d  31127  cdleme21e  31128  cdleme22e  31141  cdleme22f2  31144  cdleme22g  31145  cdleme26e  31156  cdleme28a  31167  cdleme28b  31168  cdleme37m  31259  cdleme39n  31263  cdlemeg46gfre  31329  cdlemg28a  31490  cdlemg28b  31500  cdlemk3  31630  cdlemk5a  31632  cdlemk6  31634  cdlemkuat  31663  cdlemkid2  31721
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