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  7236  grusn  8442  subeq0  9089  halfaddsub  9961  avglt2  9966  modabs2  11014  efsub  12396  sinmul  12468  divalgmod  12621  modgcd  12731  pythagtriplem4  12888  pythagtriplem16  12899  pltirr  14113  latjidm  14196  latmidm  14208  lubsn  14216  ipopos  14279  lsmss1  14991  zntoslem  16526  obsipid  16638  ordtt1  17123  xmet0  17923  nmsq  18646  tchcphlem3  18679  tchcph  18683  grpoidinvlem1  20887  grpodivid  20933  gxmodid  20962  nvmid  21239  ipidsq  21302  5oalem1  22249  3oalem2  22258  unopf1o  22512  unopnorm  22513  hmopre  22519  ballotlemfc0  23067  ballotlemfcc  23068  pdivsq  24173  gcdabsorb  24176  cgr3rflx  24749  endofsegid  24780  nnssi2  24966  nndivlub  24969  tailini  26428  pell14qrexpclnn0  27054  rmxdbl  27127  rmydbl  27128  f1omvdcnv  27490  opoccl  30006  opococ  30007  opexmid  30019  opnoncon  30020  cmtidN  30069  ltrniotaidvalN  31394
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