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

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

Proof of Theorem simp32r
StepHypRef Expression
1 simp2r 1023 . 2
213ad2ant3 1019 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  cdlema1N  35515  paddasslem15  35558  4atex2-0aOLDN  35802  4atex3  35805  cdleme19b  36030  cdleme19d  36032  cdleme19e  36033  cdleme20d  36038  cdleme20f  36040  cdleme20g  36041  cdleme21d  36056  cdleme21e  36057  cdleme22cN  36068  cdleme22e  36070  cdleme22f2  36073  cdleme26e  36085  cdleme28a  36096  cdleme37m  36188  cdlemg28b  36429  cdlemk3  36559  cdlemk12  36576  cdlemk12u  36598  cdlemkoatnle-2N  36601  cdlemk13-2N  36602  cdlemkole-2N  36603  cdlemk14-2N  36604  cdlemk15-2N  36605  cdlemk16-2N  36606  cdlemk17-2N  36607  cdlemk18-2N  36612  cdlemk19-2N  36613  cdlemk7u-2N  36614  cdlemk11u-2N  36615  cdlemk20-2N  36618  cdlemk30  36620  cdlemk23-3  36628  cdlemk24-3  36629
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