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

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

Proof of Theorem simp23r
StepHypRef Expression
1 simp3r 984 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ps )
213ad2ant2 977 1  |-  ( ( ta  /\  ( ch 
/\  th  /\  ( ph  /\  ps ) )  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  ax5seglem6  24634  lshpkrlem5  29926  lplnexllnN  30375  4atexlemutvt  30865  cdlemc5  31006  cdlemd2  31010  cdleme0moN  31036  cdleme3h  31046  cdleme5  31051  cdleme9  31064  cdleme11l  31080  cdleme14  31084  cdleme15c  31087  cdleme16b  31090  cdleme16d  31092  cdleme16e  31093  cdlemednpq  31110  cdleme20bN  31121  cdleme20j  31129  cdleme20l2  31132  cdleme20l  31133  cdleme22cN  31153  cdleme22d  31154  cdleme22e  31155  cdleme22f  31157  cdleme26fALTN  31173  cdleme26f  31174  cdleme26f2ALTN  31175  cdleme26f2  31176  cdleme27a  31178  cdleme32b  31253  cdleme32d  31255  cdleme32f  31257  cdleme39n  31277  cdleme40n  31279  cdlemg2fv2  31411  cdlemg17h  31479  cdlemg27b  31507  cdlemg28b  31514  cdlemg28  31515  cdlemg29  31516  cdlemg33a  31517  cdlemg33d  31520  cdlemk7u-2N  31699  cdlemk11u-2N  31700  cdlemk12u-2N  31701  cdlemk26-3  31717  cdlemk27-3  31718  cdlemkfid3N  31736  cdlemn11c  32021
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