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

Theorem simp23r 1079
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 986 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ps )
213ad2ant2 979 1  |-  ( ( ta  /\  ( ch 
/\  th  /\  ( ph  /\  ps ) )  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  ax5seglem6  25873  lshpkrlem5  29912  lplnexllnN  30361  4atexlemutvt  30851  cdlemc5  30992  cdlemd2  30996  cdleme0moN  31022  cdleme3h  31032  cdleme5  31037  cdleme9  31050  cdleme11l  31066  cdleme14  31070  cdleme15c  31073  cdleme16b  31076  cdleme16d  31078  cdleme16e  31079  cdlemednpq  31096  cdleme20bN  31107  cdleme20j  31115  cdleme20l2  31118  cdleme20l  31119  cdleme22cN  31139  cdleme22d  31140  cdleme22e  31141  cdleme22f  31143  cdleme26fALTN  31159  cdleme26f  31160  cdleme26f2ALTN  31161  cdleme26f2  31162  cdleme27a  31164  cdleme32b  31239  cdleme32d  31241  cdleme32f  31243  cdleme39n  31263  cdleme40n  31265  cdlemg2fv2  31397  cdlemg17h  31465  cdlemg27b  31493  cdlemg28b  31500  cdlemg28  31501  cdlemg29  31502  cdlemg33a  31503  cdlemg33d  31506  cdlemk7u-2N  31685  cdlemk11u-2N  31686  cdlemk12u-2N  31687  cdlemk26-3  31703  cdlemk27-3  31704  cdlemkfid3N  31722  cdlemn11c  32007
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator