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

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

Proof of Theorem simp23l
StepHypRef Expression
1 simp3l 983 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
213ad2ant2 977 1  |-  ( ( ta  /\  ( ch 
/\  th  /\  ( ph  /\  ps ) )  /\  et )  ->  ph )
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  4atexlemt  30864  4atex2  30888  4atex3  30892  trlval4  30999  cdlemc5  31006  cdlemc6  31007  cdlemd2  31010  cdleme0e  31028  cdleme0moN  31036  cdleme3g  31045  cdleme3h  31046  cdleme3  31048  cdleme4  31049  cdleme5  31051  cdleme9  31064  cdleme11fN  31075  cdleme11j  31078  cdleme11k  31079  cdleme11l  31080  cdleme11  31081  cdleme14  31084  cdleme15a  31085  cdleme15b  31086  cdleme15c  31087  cdleme16b  31090  cdleme16c  31091  cdleme16d  31092  cdleme16e  31093  cdleme16f  31094  cdleme17d1  31100  cdleme18c  31104  cdlemednpq  31110  cdleme19c  31116  cdleme20bN  31121  cdleme20d  31123  cdleme20f  31125  cdleme20g  31126  cdleme20h  31127  cdleme20j  31129  cdleme20l2  31132  cdleme20l  31133  cdleme20m  31134  cdleme22cN  31153  cdleme22d  31154  cdleme22e  31155  cdleme22f  31157  cdleme26fALTN  31173  cdleme26f  31174  cdleme26f2ALTN  31175  cdleme26f2  31176  cdleme27a  31178  cdleme28a  31181  cdlemefs44  31237  cdlemefs45ee  31241  cdleme32b  31253  cdleme32c  31254  cdleme32e  31256  cdleme35sn2aw  31269  cdleme37m  31273  cdleme39n  31277  cdleme40n  31279  cdleme40w  31281  cdleme42k  31295  cdlemeg47rv2  31321  cdlemeg46rjgN  31333  cdlemeg46rgv  31339  cdlemeg46req  31340  cdlemg2fv2  31411  cdlemg17h  31479  cdlemg31b0a  31506  cdlemg27b  31507  cdlemg31d  31511  cdlemg28b  31514  cdlemg28  31515  cdlemg29  31516  cdlemg33a  31517  cdlemg33b  31518  cdlemg33c  31519  cdlemg33d  31520  cdlemg33e  31521  cdlemg44a  31542  cdlemk7u-2N  31699  cdlemk11u-2N  31700  cdlemk12u-2N  31701  cdlemk26-3  31717  cdlemk27-3  31718  cdlemkfid3N  31736  cdlemn2  32007  cdlemn10  32018  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