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  24677  cdleme19b  31038  cdleme19d  31040  cdleme19e  31041  cdleme20h  31050  cdleme20l2  31055  cdleme20m  31057  cdleme21d  31064  cdleme21e  31065  cdleme22e  31078  cdleme22f2  31081  cdleme22g  31082  cdleme26e  31093  cdleme28a  31104  cdleme28b  31105  cdleme37m  31196  cdleme39n  31200  cdlemeg46gfre  31266  cdlemg28a  31427  cdlemg28b  31437  cdlemk3  31567  cdlemk5a  31569  cdlemk6  31571  cdlemkuat  31600  cdlemkid2  31658
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