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

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

Proof of Theorem simp21r
StepHypRef Expression
1 simp1r 1021 . 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  cdleme0moN  35950  cdleme16e  36007  cdleme17d1  36014  cdleme18d  36020  cdleme19d  36032  cdleme20f  36040  cdleme20g  36041  cdleme21ct  36055  cdleme22aa  36065  cdleme22cN  36068  cdleme22d  36069  cdleme22e  36070  cdleme22eALTN  36071  cdleme26e  36085  cdleme32e  36171  cdleme32f  36172  cdlemg4  36343  cdlemg18d  36407  cdlemg18  36408  cdlemg19a  36409  cdlemg19  36410  cdlemg21  36412  cdlemg33b0  36427  cdlemk5  36562  cdlemk6  36563  cdlemk7  36574  cdlemk11  36575  cdlemk12  36576  cdlemk21N  36599  cdlemk20  36600  cdlemk28-3  36634  cdlemk34  36636  cdlemkfid3N  36651  cdlemk55u1  36691
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