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

Theorem simp33r 1083
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp33r  |-  ( ( ta  /\  et  /\  ( ch  /\  th  /\  ( ph  /\  ps )
) )  ->  ps )

Proof of Theorem simp33r
StepHypRef Expression
1 simp3r 984 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ps )
213ad2ant3 978 1  |-  ( ( ta  /\  et  /\  ( ch  /\  th  /\  ( ph  /\  ps )
) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  totprob  23645  cdleme19b  31115  cdleme19e  31118  cdleme20h  31127  cdleme20l2  31132  cdleme20m  31134  cdleme21d  31141  cdleme21e  31142  cdleme22eALTN  31156  cdleme22f2  31158  cdleme22g  31159  cdleme26e  31170  cdleme37m  31273  cdlemeg46gfre  31343  cdlemg28a  31504  cdlemg28b  31514  cdlemk5a  31646  cdlemk6  31648
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