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

Theorem 3anidm23 1532
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 1112 . 2 (((𝜑𝜓) ∧ 𝜓) → 𝜒)
32anabss3 899 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  supsn  8545  infsn  8577  grusn  9838  subeq0  10519  halfaddsub  11477  avglt2  11483  modabs2  12918  efsub  15049  sinmul  15121  divalgmod  15351  divalgmodOLD  15352  modgcd  15475  pythagtriplem4  15746  pythagtriplem16  15757  pltirr  17184  latjidm  17295  latmidm  17307  ipopos  17381  mulgmodid  17802  f1omvdcnv  18084  lsmss1  18299  zntoslem  20127  obsipid  20288  smadiadetlem2  20692  smadiadet  20698  ordtt1  21405  xmet0  22368  nmsq  23214  tchcphlem3  23252  tchcph  23256  grpoidinvlem1  27688  grpodivid  27726  nvmid  27844  ipidsq  27895  5oalem1  28843  3oalem2  28852  unopf1o  29105  unopnorm  29106  hmopre  29112  ballotlemfc0  30884  ballotlemfcc  30885  pdivsq  31963  gcdabsorb  31966  cgr3rflx  32488  endofsegid  32519  tailini  32698  nnssi2  32781  nndivlub  32784  brin2  34508  opoccl  35002  opococ  35003  opexmid  35015  opnoncon  35016  cmtidN  35065  ltrniotaidvalN  36391  pell14qrexpclnn0  37950  rmxdbl  38024  rmydbl  38025  rhmsubclem3  42616  rhmsubcALTVlem3  42634
  Copyright terms: Public domain W3C validator