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

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

Proof of Theorem simp31r
StepHypRef Expression
1 simp1r 1021 . 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  cdlemednpq  36024  cdleme19e  36033  cdleme20h  36042  cdleme20j  36044  cdleme20l2  36047  cdleme20m  36049  cdleme22a  36066  cdleme22cN  36068  cdleme22f2  36073  cdleme26f2ALTN  36090  cdleme37m  36188  cdlemg12f  36374  cdlemg12g  36375  cdlemg12  36376  cdlemg28a  36419  cdlemg29  36431  cdlemg33a  36432  cdlemg36  36440  cdlemk16a  36582  cdlemk21-2N  36617  cdlemk54  36684  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