MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp23r 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  25777  lshpkrlem5  29597  lplnexllnN  30046  4atexlemutvt  30536  cdlemc5  30677  cdlemd2  30681  cdleme0moN  30707  cdleme3h  30717  cdleme5  30722  cdleme9  30735  cdleme11l  30751  cdleme14  30755  cdleme15c  30758  cdleme16b  30761  cdleme16d  30763  cdleme16e  30764  cdlemednpq  30781  cdleme20bN  30792  cdleme20j  30800  cdleme20l2  30803  cdleme20l  30804  cdleme22cN  30824  cdleme22d  30825  cdleme22e  30826  cdleme22f  30828  cdleme26fALTN  30844  cdleme26f  30845  cdleme26f2ALTN  30846  cdleme26f2  30847  cdleme27a  30849  cdleme32b  30924  cdleme32d  30926  cdleme32f  30928  cdleme39n  30948  cdleme40n  30950  cdlemg2fv2  31082  cdlemg17h  31150  cdlemg27b  31178  cdlemg28b  31185  cdlemg28  31186  cdlemg29  31187  cdlemg33a  31188  cdlemg33d  31191  cdlemk7u-2N  31370  cdlemk11u-2N  31371  cdlemk12u-2N  31372  cdlemk26-3  31388  cdlemk27-3  31389  cdlemkfid3N  31407  cdlemn11c  31692
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