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

Theorem 3anidm23 1382
Description: Inference from idempotent law for conjunction. (Contributed by NM, 1-Feb-2007.)
Hypothesis
Ref Expression
3anidm23.1 ((𝜑𝜓𝜓) → 𝜒)
Assertion
Ref Expression
3anidm23 ((𝜑𝜓) → 𝜒)

Proof of Theorem 3anidm23
StepHypRef Expression
1 3anidm23.1 . . 3 ((𝜑𝜓𝜓) → 𝜒)
213expa 1262 . 2 (((𝜑𝜓) ∧ 𝜓) → 𝜒)
32anabss3 863 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  supsn  8322  infsn  8354  grusn  9570  subeq0  10251  halfaddsub  11209  avglt2  11215  modabs2  12644  efsub  14755  sinmul  14827  divalgmod  15053  divalgmodOLD  15054  modgcd  15177  pythagtriplem4  15448  pythagtriplem16  15459  pltirr  16884  latjidm  16995  latmidm  17007  ipopos  17081  mulgmodid  17502  f1omvdcnv  17785  lsmss1  18000  zntoslem  19824  obsipid  19985  smadiadetlem2  20389  smadiadet  20395  ordtt1  21093  xmet0  22057  nmsq  22902  tchcphlem3  22940  tchcph  22944  grpoidinvlem1  27204  grpodivid  27242  nvmid  27360  ipidsq  27411  5oalem1  28359  3oalem2  28368  unopf1o  28621  unopnorm  28622  hmopre  28628  ballotlemfc0  30332  ballotlemfcc  30333  pdivsq  31340  gcdabsorb  31343  fv2ndcnv  31380  cgr3rflx  31800  endofsegid  31831  tailini  32010  nnssi2  32093  nndivlub  32096  opoccl  33958  opococ  33959  opexmid  33971  opnoncon  33972  cmtidN  34021  ltrniotaidvalN  35348  pell14qrexpclnn0  36907  rmxdbl  36981  rmydbl  36982  rhmsubclem3  41373  rhmsubcALTVlem3  41391
  Copyright terms: Public domain W3C validator