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

Theorem simp33l 1082
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 983 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
213ad2ant3 978 1  |-  ( ( ta  /\  et  /\  ( ch  /\  th  /\  ( ph  /\  ps )
) )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  totprob  23630  cdleme19b  30493  cdleme19d  30495  cdleme19e  30496  cdleme20h  30505  cdleme20l2  30510  cdleme20m  30512  cdleme21d  30519  cdleme21e  30520  cdleme22e  30533  cdleme22f2  30536  cdleme22g  30537  cdleme26e  30548  cdleme28a  30559  cdleme28b  30560  cdleme37m  30651  cdleme39n  30655  cdlemeg46gfre  30721  cdlemg28a  30882  cdlemg28b  30892  cdlemk3  31022  cdlemk5a  31024  cdlemk6  31026  cdlemkuat  31055  cdlemkid2  31113
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator