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

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

Proof of Theorem simp33r
StepHypRef Expression
1 simp3r 1025 . 2
213ad2ant3 1019 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  totprob  28366  cdleme19b  36030  cdleme19e  36033  cdleme20h  36042  cdleme20l2  36047  cdleme20m  36049  cdleme21d  36056  cdleme21e  36057  cdleme22eALTN  36071  cdleme22f2  36073  cdleme22g  36074  cdleme26e  36085  cdleme37m  36188  cdlemeg46gfre  36258  cdlemg28a  36419  cdlemg28b  36429  cdlemk5a  36561  cdlemk6  36563
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