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

Theorem 3anidm23 1277
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 1187 . 2  |-  ( ( ( ph  /\  ps )  /\  ps )  ->  ch )
32anabss3 819 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  supsn  7719  grusn  8971  subeq0  9635  halfaddsub  10558  avglt2  10563  modabs2  11742  efsub  13384  sinmul  13456  divalgmod  13610  modgcd  13720  pythagtriplem4  13886  pythagtriplem16  13897  pltirr  15133  latjidm  15244  latmidm  15256  ipopos  15330  f1omvdcnv  15950  lsmss1  16163  zntoslem  17989  obsipid  18147  smadiadetlem2  18470  smadiadet  18476  ordtt1  18983  xmet0  19917  nmsq  20713  tchcphlem3  20748  tchcph  20752  grpoidinvlem1  23691  grpodivid  23737  gxmodid  23766  nvmid  24045  ipidsq  24108  5oalem1  25057  3oalem2  25066  unopf1o  25320  unopnorm  25321  hmopre  25327  ballotlemfc0  26875  ballotlemfcc  26876  pdivsq  27555  gcdabsorb  27558  cgr3rflx  28085  endofsegid  28116  nnssi2  28301  nndivlub  28304  tailini  28597  pell14qrexpclnn0  29207  rmxdbl  29280  rmydbl  29281  opoccl  32839  opococ  32840  opexmid  32852  opnoncon  32853  cmtidN  32902  ltrniotaidvalN  34227
  Copyright terms: Public domain W3C validator