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

Theorem 3anidm23 1244
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 1154 . 2  |-  ( ( ( ph  /\  ps )  /\  ps )  ->  ch )
32anabss3 798 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  supsn  7475  grusn  8680  subeq0  9328  halfaddsub  10202  avglt2  10207  modabs2  11276  efsub  12702  sinmul  12774  divalgmod  12927  modgcd  13037  pythagtriplem4  13194  pythagtriplem16  13205  pltirr  14421  latjidm  14504  latmidm  14516  lubsn  14524  ipopos  14587  lsmss1  15299  zntoslem  16838  obsipid  16950  ordtt1  17444  xmet0  18373  nmsq  19158  tchcphlem3  19191  tchcph  19195  grpoidinvlem1  21793  grpodivid  21839  gxmodid  21868  nvmid  22147  ipidsq  22210  5oalem1  23157  3oalem2  23166  unopf1o  23420  unopnorm  23421  hmopre  23427  ballotlemfc0  24751  ballotlemfcc  24752  pdivsq  25369  gcdabsorb  25372  cgr3rflx  25989  endofsegid  26020  nnssi2  26206  nndivlub  26209  tailini  26406  pell14qrexpclnn0  26930  rmxdbl  27003  rmydbl  27004  f1omvdcnv  27365  opoccl  29993  opococ  29994  opexmid  30006  opnoncon  30007  cmtidN  30056  ltrniotaidvalN  31381
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator