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

Theorem simp21r 1075
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp21r  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )  /\  et )  ->  ps )

Proof of Theorem simp21r
StepHypRef Expression
1 simp1r 982 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
213ad2ant2 979 1  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  modexp  11441  segconeu  25659  4atlem10  29720  lplncvrlvol2  29729  4atex  30190  4atex2-0cOLDN  30194  cdleme0moN  30339  cdleme16e  30396  cdleme17d1  30403  cdleme18d  30409  cdleme19d  30420  cdleme20f  30428  cdleme20g  30429  cdleme21ct  30443  cdleme22aa  30453  cdleme22cN  30456  cdleme22d  30457  cdleme22e  30458  cdleme22eALTN  30459  cdleme26e  30473  cdleme32e  30559  cdleme32f  30560  cdlemg4  30731  cdlemg18d  30795  cdlemg18  30796  cdlemg19a  30797  cdlemg19  30798  cdlemg21  30800  cdlemg33b0  30815  cdlemk5  30950  cdlemk6  30951  cdlemk7  30962  cdlemk11  30963  cdlemk12  30964  cdlemk21N  30987  cdlemk20  30988  cdlemk28-3  31022  cdlemk34  31024  cdlemkfid3N  31039  cdlemk55u1  31079
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