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

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

Proof of Theorem simp21l
StepHypRef Expression
1 simp1l 1020 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
213ad2ant2 1018 1  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )  /\  et )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 975
This theorem is referenced by:  modexp  12265  segconeu  29238  4atlem10  34402  lplncvrlvol2  34411  4atex  34872  4atex2-0cOLDN  34876  cdlemd2  34995  cdlemd3  34996  cdlemd4  34997  cdleme0e  35013  cdleme0moN  35021  cdleme3g  35030  cdleme3h  35031  cdleme3  35033  cdleme9  35049  cdleme11c  35057  cdleme11dN  35058  cdleme11e  35059  cdleme11fN  35060  cdleme11h  35062  cdleme11j  35063  cdleme11k  35064  cdleme11  35066  cdleme12  35067  cdleme13  35068  cdleme14  35069  cdleme15a  35070  cdleme15b  35071  cdleme15c  35072  cdleme15d  35073  cdleme15  35074  cdleme16b  35075  cdleme16c  35076  cdleme16d  35077  cdleme16e  35078  cdleme16f  35079  cdleme17d1  35085  cdleme18a  35087  cdleme18b  35088  cdleme18c  35089  cdleme18d  35091  cdleme19b  35100  cdleme19d  35102  cdleme19e  35103  cdleme20c  35107  cdleme20d  35108  cdleme20e  35109  cdleme20f  35110  cdleme20g  35111  cdleme20h  35112  cdleme20j  35114  cdleme20l2  35117  cdleme20l  35118  cdleme20m  35119  cdleme20  35120  cdleme21ct  35125  cdleme21e  35127  cdleme21i  35131  cdleme22aa  35135  cdleme22cN  35138  cdleme22d  35139  cdleme22e  35140  cdleme22eALTN  35141  cdleme22f  35142  cdleme26e  35155  cdleme27a  35163  cdleme32e  35241  cdlemg2fv2  35396  cdlemg4a  35404  cdlemg4d  35409  cdlemg4  35413  cdlemg6c  35416  cdlemg8b  35424  cdlemg8c  35425  cdlemg9a  35428  cdlemg9  35430  cdlemg12a  35439  cdlemg12c  35441  cdlemg17dALTN  35460  cdlemg17h  35464  cdlemg18b  35475  cdlemg18c  35476  cdlemg18d  35477  cdlemg18  35478  cdlemg19a  35479  cdlemg21  35482  cdlemg28a  35489  cdlemg31b0a  35491  cdlemg31d  35496  cdlemg33b0  35497  cdlemg33a  35502  cdlemh  35613  cdlemk5  35632  cdlemk6  35633  cdlemk7  35644  cdlemk11  35645  cdlemk12  35646  cdlemk21N  35669  cdlemk20  35670  cdlemk28-3  35704  cdlemk34  35706  cdlemkfid3N  35721  cdlemk35s-id  35734  cdlemk39s-id  35736  cdlemk55u1  35761  cdlemn2  35992  cdlemn10  36003  dihjustlem  36013
  Copyright terms: Public domain W3C validator