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

Theorem 3anidm23 1241
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 1151 . 2  |-  ( ( ( ph  /\  ps )  /\  ps )  ->  ch )
32anabss3 796 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  supsn  7220  grusn  8426  subeq0  9073  halfaddsub  9945  avglt2  9950  modabs2  10998  efsub  12380  sinmul  12452  divalgmod  12605  modgcd  12715  pythagtriplem4  12872  pythagtriplem16  12883  pltirr  14097  latjidm  14180  latmidm  14192  lubsn  14200  ipopos  14263  lsmss1  14975  zntoslem  16510  obsipid  16622  ordtt1  17107  xmet0  17907  nmsq  18630  tchcphlem3  18663  tchcph  18667  grpoidinvlem1  20871  grpodivid  20917  gxmodid  20946  nvmid  21223  ipidsq  21286  5oalem1  22233  3oalem2  22242  unopf1o  22496  unopnorm  22497  hmopre  22503  ballotlemfc0  23051  ballotlemfcc  23052  pdivsq  24102  gcdabsorb  24105  cgr3rflx  24677  endofsegid  24708  nnssi2  24894  nndivlub  24897  tailini  26325  pell14qrexpclnn0  26951  rmxdbl  27024  rmydbl  27025  f1omvdcnv  27387  opoccl  29384  opococ  29385  opexmid  29397  opnoncon  29398  cmtidN  29447  ltrniotaidvalN  30772
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator