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  23630  cdleme19b  30493  cdleme19e  30496  cdleme20h  30505  cdleme20l2  30510  cdleme20m  30512  cdleme21d  30519  cdleme21e  30520  cdleme22eALTN  30534  cdleme22f2  30536  cdleme22g  30537  cdleme26e  30548  cdleme37m  30651  cdlemeg46gfre  30721  cdlemg28a  30882  cdlemg28b  30892  cdlemk5a  31024  cdlemk6  31026
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