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

Theorem 3anidm23 1282
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 1191 . 2  |-  ( ( ( ph  /\  ps )  /\  ps )  ->  ch )
32anabss3 820 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 968
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 970
This theorem is referenced by:  supsn  7919  grusn  9171  subeq0  9834  halfaddsub  10761  avglt2  10766  modabs2  11986  efsub  13685  sinmul  13757  divalgmod  13912  modgcd  14022  pythagtriplem4  14191  pythagtriplem16  14202  pltirr  15439  latjidm  15550  latmidm  15562  ipopos  15636  f1omvdcnv  16258  lsmss1  16473  zntoslem  18355  obsipid  18513  smadiadetlem2  18926  smadiadet  18932  ordtt1  19639  xmet0  20573  nmsq  21369  tchcphlem3  21404  tchcph  21408  grpoidinvlem1  24868  grpodivid  24914  gxmodid  24943  nvmid  25222  ipidsq  25285  5oalem1  26234  3oalem2  26243  unopf1o  26497  unopnorm  26498  hmopre  26504  ballotlemfc0  28057  ballotlemfcc  28058  pdivsq  28737  gcdabsorb  28740  cgr3rflx  29267  endofsegid  29298  nnssi2  29483  nndivlub  29486  tailini  29784  pell14qrexpclnn0  30393  rmxdbl  30466  rmydbl  30467  opoccl  33866  opococ  33867  opexmid  33879  opnoncon  33880  cmtidN  33929  ltrniotaidvalN  35254
  Copyright terms: Public domain W3C validator