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

Theorem simp23r 1116
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 1023 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ps )
213ad2ant2 1016 1  |-  ( ( ta  /\  ( ch 
/\  th  /\  ( ph  /\  ps ) )  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  ax5seglem6  24439  lshpkrlem5  35236  lplnexllnN  35685  4atexlemutvt  36175  cdlemc5  36317  cdlemd2  36321  cdleme0moN  36347  cdleme3h  36357  cdleme5  36362  cdleme9  36375  cdleme11l  36391  cdleme14  36395  cdleme15c  36398  cdleme16b  36401  cdleme16d  36403  cdleme16e  36404  cdlemednpq  36421  cdleme20bN  36433  cdleme20j  36441  cdleme20l2  36444  cdleme20l  36445  cdleme22cN  36465  cdleme22d  36466  cdleme22e  36467  cdleme22f  36469  cdleme26fALTN  36485  cdleme26f  36486  cdleme26f2ALTN  36487  cdleme26f2  36488  cdleme27a  36490  cdleme32b  36565  cdleme32d  36567  cdleme32f  36569  cdleme39n  36589  cdleme40n  36591  cdlemg2fv2  36723  cdlemg17h  36791  cdlemg27b  36819  cdlemg28b  36826  cdlemg28  36827  cdlemg29  36828  cdlemg33a  36829  cdlemg33d  36832  cdlemk7u-2N  37011  cdlemk11u-2N  37012  cdlemk12u-2N  37013  cdlemk26-3  37029  cdlemk27-3  37030  cdlemkfid3N  37048  cdlemn11c  37333
  Copyright terms: Public domain W3C validator