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  24638  cdleme19b  30786  cdleme19d  30788  cdleme19e  30789  cdleme20h  30798  cdleme20l2  30803  cdleme20m  30805  cdleme21d  30812  cdleme21e  30813  cdleme22e  30826  cdleme22f2  30829  cdleme22g  30830  cdleme26e  30841  cdleme28a  30852  cdleme28b  30853  cdleme37m  30944  cdleme39n  30948  cdlemeg46gfre  31014  cdlemg28a  31175  cdlemg28b  31185  cdlemk3  31315  cdlemk5a  31317  cdlemk6  31319  cdlemkuat  31348  cdlemkid2  31406
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