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

Theorem 3anidm23 1289
Description: Inference from idempotent law for conjunction. (Contributed by NM, 1-Feb-2007.)
Hypothesis
Ref Expression
3anidm23.1  |-  ( (
ph  /\  ps  /\  ps )  ->  ch )
Assertion
Ref Expression
3anidm23  |-  ( (
ph  /\  ps )  ->  ch )

Proof of Theorem 3anidm23
StepHypRef Expression
1 3anidm23.1 . . 3  |-  ( (
ph  /\  ps  /\  ps )  ->  ch )
213expa 1197 . 2  |-  ( ( ( ph  /\  ps )  /\  ps )  ->  ch )
32anabss3 824 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 974
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 369  df-3an 976
This theorem is referenced by:  supsn  7963  grusn  9211  subeq0  9880  halfaddsub  10812  avglt2  10817  modabs2  12067  efsub  14042  sinmul  14114  divalgmod  14271  modgcd  14381  pythagtriplem4  14550  pythagtriplem16  14561  pltirr  15915  latjidm  16026  latmidm  16038  ipopos  16112  f1omvdcnv  16791  lsmss1  17006  zntoslem  18891  obsipid  19049  smadiadetlem2  19456  smadiadet  19462  ordtt1  20171  xmet0  21135  nmsq  21931  tchcphlem3  21966  tchcph  21970  grpoidinvlem1  25606  grpodivid  25652  gxmodid  25681  nvmid  25960  ipidsq  26023  5oalem1  26972  3oalem2  26981  unopf1o  27234  unopnorm  27235  hmopre  27241  ballotlemfc0  28923  ballotlemfcc  28924  pdivsq  29945  gcdabsorb  29948  fv2ndcnv  29983  cgr3rflx  30379  endofsegid  30410  tailini  30591  nnssi2  30674  nndivlub  30677  opoccl  32192  opococ  32193  opexmid  32205  opnoncon  32206  cmtidN  32255  ltrniotaidvalN  33582  pell14qrexpclnn0  35143  rmxdbl  35216  rmydbl  35217  rhmsubclem3  38388  rhmsubcALTVlem3  38407
  Copyright terms: Public domain W3C validator