MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp33l 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  24466  cdleme19b  30420  cdleme19d  30422  cdleme19e  30423  cdleme20h  30432  cdleme20l2  30437  cdleme20m  30439  cdleme21d  30446  cdleme21e  30447  cdleme22e  30460  cdleme22f2  30463  cdleme22g  30464  cdleme26e  30475  cdleme28a  30486  cdleme28b  30487  cdleme37m  30578  cdleme39n  30582  cdlemeg46gfre  30648  cdlemg28a  30809  cdlemg28b  30819  cdlemk3  30949  cdlemk5a  30951  cdlemk6  30953  cdlemkuat  30982  cdlemkid2  31040
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