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

Theorem 3anidm23 1287
Description: Inference from idempotent law for conjunction. (Contributed by NM, 1-Feb-2007.)
Hypothesis
Ref Expression
3anidm23.1
Assertion
Ref Expression
3anidm23

Proof of Theorem 3anidm23
StepHypRef Expression
1 3anidm23.1 . . 3
213expa 1196 . 2
32anabss3 823 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  supsn  7951  grusn  9203  subeq0  9868  halfaddsub  10797  avglt2  10802  modabs2  12030  efsub  13835  sinmul  13907  divalgmod  14064  modgcd  14174  pythagtriplem4  14343  pythagtriplem16  14354  pltirr  15593  latjidm  15704  latmidm  15716  ipopos  15790  f1omvdcnv  16469  lsmss1  16684  zntoslem  18595  obsipid  18753  smadiadetlem2  19166  smadiadet  19172  ordtt1  19880  xmet0  20845  nmsq  21641  tchcphlem3  21676  tchcph  21680  grpoidinvlem1  25206  grpodivid  25252  gxmodid  25281  nvmid  25560  ipidsq  25623  5oalem1  26572  3oalem2  26581  unopf1o  26835  unopnorm  26836  hmopre  26842  ballotlemfc0  28431  ballotlemfcc  28432  pdivsq  29174  gcdabsorb  29177  cgr3rflx  29704  endofsegid  29735  nnssi2  29920  nndivlub  29923  tailini  30194  pell14qrexpclnn0  30802  rmxdbl  30875  rmydbl  30876  rhmsubclem3  32896  rhmsubcOLDlem3  32915  opoccl  34919  opococ  34920  opexmid  34932  opnoncon  34933  cmtidN  34982  ltrniotaidvalN  36309
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