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

Theorem simp21l 1113
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp21l

Proof of Theorem simp21l
StepHypRef Expression
1 simp1l 1020 . 2
213ad2ant2 1018 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  modexp  12301  segconeu  29661  4atlem10  35330  lplncvrlvol2  35339  4atex  35800  4atex2-0cOLDN  35804  cdlemd2  35924  cdlemd3  35925  cdlemd4  35926  cdleme0e  35942  cdleme0moN  35950  cdleme3g  35959  cdleme3h  35960  cdleme3  35962  cdleme9  35978  cdleme11c  35986  cdleme11dN  35987  cdleme11e  35988  cdleme11fN  35989  cdleme11h  35991  cdleme11j  35992  cdleme11k  35993  cdleme11  35995  cdleme12  35996  cdleme13  35997  cdleme14  35998  cdleme15a  35999  cdleme15b  36000  cdleme15c  36001  cdleme15d  36002  cdleme15  36003  cdleme16b  36004  cdleme16c  36005  cdleme16d  36006  cdleme16e  36007  cdleme16f  36008  cdleme17d1  36014  cdleme18a  36016  cdleme18b  36017  cdleme18c  36018  cdleme18d  36020  cdleme19b  36030  cdleme19d  36032  cdleme19e  36033  cdleme20c  36037  cdleme20d  36038  cdleme20e  36039  cdleme20f  36040  cdleme20g  36041  cdleme20h  36042  cdleme20j  36044  cdleme20l2  36047  cdleme20l  36048  cdleme20m  36049  cdleme20  36050  cdleme21ct  36055  cdleme21e  36057  cdleme21i  36061  cdleme22aa  36065  cdleme22cN  36068  cdleme22d  36069  cdleme22e  36070  cdleme22eALTN  36071  cdleme22f  36072  cdleme26e  36085  cdleme27a  36093  cdleme32e  36171  cdlemg2fv2  36326  cdlemg4a  36334  cdlemg4d  36339  cdlemg4  36343  cdlemg6c  36346  cdlemg8b  36354  cdlemg8c  36355  cdlemg9a  36358  cdlemg9  36360  cdlemg12a  36369  cdlemg12c  36371  cdlemg17dALTN  36390  cdlemg17h  36394  cdlemg18b  36405  cdlemg18c  36406  cdlemg18d  36407  cdlemg18  36408  cdlemg19a  36409  cdlemg21  36412  cdlemg28a  36419  cdlemg31b0a  36421  cdlemg31d  36426  cdlemg33b0  36427  cdlemg33a  36432  cdlemh  36543  cdlemk5  36562  cdlemk6  36563  cdlemk7  36574  cdlemk11  36575  cdlemk12  36576  cdlemk21N  36599  cdlemk20  36600  cdlemk28-3  36634  cdlemk34  36636  cdlemkfid3N  36651  cdlemk35s-id  36664  cdlemk39s-id  36666  cdlemk55u1  36691  cdlemn2  36922  cdlemn10  36933  dihjustlem  36943
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
  Copyright terms: Public domain W3C validator