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  23645  cdleme19b  31115  cdleme19d  31117  cdleme19e  31118  cdleme20h  31127  cdleme20l2  31132  cdleme20m  31134  cdleme21d  31141  cdleme21e  31142  cdleme22e  31155  cdleme22f2  31158  cdleme22g  31159  cdleme26e  31170  cdleme28a  31181  cdleme28b  31182  cdleme37m  31273  cdleme39n  31277  cdlemeg46gfre  31343  cdlemg28a  31504  cdlemg28b  31514  cdlemk3  31644  cdlemk5a  31646  cdlemk6  31648  cdlemkuat  31677  cdlemkid2  31735
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