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

Theorem simp23l 1117
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 1024 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
213ad2ant2 1018 1  |-  ( ( ta  /\  ( ch 
/\  th  /\  ( ph  /\  ps ) )  /\  et )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975
This theorem is referenced by:  ax5seglem6  23913  lshpkrlem5  33911  lplnexllnN  34360  4atexlemt  34849  4atex2  34873  4atex3  34877  trlval4  34984  cdlemc5  34991  cdlemc6  34992  cdlemd2  34995  cdleme0e  35013  cdleme0moN  35021  cdleme3g  35030  cdleme3h  35031  cdleme3  35033  cdleme4  35034  cdleme5  35036  cdleme9  35049  cdleme11fN  35060  cdleme11j  35063  cdleme11k  35064  cdleme11l  35065  cdleme11  35066  cdleme14  35069  cdleme15a  35070  cdleme15b  35071  cdleme15c  35072  cdleme16b  35075  cdleme16c  35076  cdleme16d  35077  cdleme16e  35078  cdleme16f  35079  cdleme17d1  35085  cdleme18c  35089  cdlemednpq  35095  cdleme19c  35101  cdleme20bN  35106  cdleme20d  35108  cdleme20f  35110  cdleme20g  35111  cdleme20h  35112  cdleme20j  35114  cdleme20l2  35117  cdleme20l  35118  cdleme20m  35119  cdleme22cN  35138  cdleme22d  35139  cdleme22e  35140  cdleme22f  35142  cdleme26fALTN  35158  cdleme26f  35159  cdleme26f2ALTN  35160  cdleme26f2  35161  cdleme27a  35163  cdleme28a  35166  cdlemefs44  35222  cdlemefs45ee  35226  cdleme32b  35238  cdleme32c  35239  cdleme32e  35241  cdleme35sn2aw  35254  cdleme37m  35258  cdleme39n  35262  cdleme40n  35264  cdleme40w  35266  cdleme42k  35280  cdlemeg47rv2  35306  cdlemeg46rjgN  35318  cdlemeg46rgv  35324  cdlemeg46req  35325  cdlemg2fv2  35396  cdlemg17h  35464  cdlemg31b0a  35491  cdlemg27b  35492  cdlemg31d  35496  cdlemg28b  35499  cdlemg28  35500  cdlemg29  35501  cdlemg33a  35502  cdlemg33b  35503  cdlemg33c  35504  cdlemg33d  35505  cdlemg33e  35506  cdlemg44a  35527  cdlemk7u-2N  35684  cdlemk11u-2N  35685  cdlemk12u-2N  35686  cdlemk26-3  35702  cdlemk27-3  35703  cdlemkfid3N  35721  cdlemn2  35992  cdlemn10  36003  cdlemn11c  36006
  Copyright terms: Public domain W3C validator