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

Theorem simp23r 1110
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 1017 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ps )
213ad2ant2 1010 1  |-  ( ( ta  /\  ( ch 
/\  th  /\  ( ph  /\  ps ) )  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  ax5seglem6  23131  lshpkrlem5  32599  lplnexllnN  33048  4atexlemutvt  33538  cdlemc5  33679  cdlemd2  33683  cdleme0moN  33709  cdleme3h  33719  cdleme5  33724  cdleme9  33737  cdleme11l  33753  cdleme14  33757  cdleme15c  33760  cdleme16b  33763  cdleme16d  33765  cdleme16e  33766  cdlemednpq  33783  cdleme20bN  33794  cdleme20j  33802  cdleme20l2  33805  cdleme20l  33806  cdleme22cN  33826  cdleme22d  33827  cdleme22e  33828  cdleme22f  33830  cdleme26fALTN  33846  cdleme26f  33847  cdleme26f2ALTN  33848  cdleme26f2  33849  cdleme27a  33851  cdleme32b  33926  cdleme32d  33928  cdleme32f  33930  cdleme39n  33950  cdleme40n  33952  cdlemg2fv2  34084  cdlemg17h  34152  cdlemg27b  34180  cdlemg28b  34187  cdlemg28  34188  cdlemg29  34189  cdlemg33a  34190  cdlemg33d  34193  cdlemk7u-2N  34372  cdlemk11u-2N  34373  cdlemk12u-2N  34374  cdlemk26-3  34390  cdlemk27-3  34391  cdlemkfid3N  34409  cdlemn11c  34694
  Copyright terms: Public domain W3C validator