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

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

Proof of Theorem simp31l
StepHypRef Expression
1 simp1l 1020 . 2
213ad2ant3 1019 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  ps-2c  35252  cdlema1N  35515  trlval3  35912  cdleme12  35996  cdlemednpq  36024  cdleme19d  36032  cdleme19e  36033  cdleme20f  36040  cdleme20h  36042  cdleme20l2  36047  cdleme20l  36048  cdleme20m  36049  cdleme21j  36062  cdleme22a  36066  cdleme22cN  36068  cdleme22f2  36073  cdleme32b  36168  cdlemg12f  36374  cdlemg12g  36375  cdlemg12  36376  cdlemg28a  36419  cdlemg31b0N  36420  cdlemg29  36431  cdlemg33a  36432  cdlemg36  36440  cdlemg42  36455  cdlemk16a  36582  cdlemk21-2N  36617  cdlemk32  36623  cdlemkid2  36650  cdlemk54  36684  cdlemk55a  36685  dihord10  36950
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