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

Theorem 3anidm23 1545
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 1148 . 2 (((𝜑𝜓) ∧ 𝜓) → 𝜒)
32anabss3 666 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  w3a 1108
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 199  df-an 386  df-3an 1110
This theorem is referenced by:  supsn  8620  infsn  8652  grusn  9914  subeq0  10599  halfaddsub  11553  avglt2  11559  modabs2  12959  efsub  15166  sinmul  15238  divalgmod  15465  modgcd  15588  pythagtriplem4  15857  pythagtriplem16  15868  pltirr  17278  latjidm  17389  latmidm  17401  ipopos  17475  mulgmodid  17894  f1omvdcnv  18176  lsmss1  18392  zntoslem  20226  obsipid  20391  smadiadetlem2  20797  smadiadet  20803  ordtt1  21512  xmet0  22475  nmsq  23321  tcphcphlem3  23359  tcphcph  23363  grpoidinvlem1  27884  grpodivid  27922  nvmid  28039  ipidsq  28090  5oalem1  29038  3oalem2  29047  unopf1o  29300  unopnorm  29301  hmopre  29307  ballotlemfc0  31071  ballotlemfcc  31072  pdivsq  32149  gcdabsorb  32152  cgr3rflx  32674  endofsegid  32705  tailini  32883  nnssi2  32962  nndivlub  32965  brin2  34661  opoccl  35215  opococ  35216  opexmid  35228  opnoncon  35229  cmtidN  35278  ltrniotaidvalN  36604  pell14qrexpclnn0  38216  rmxdbl  38289  rmydbl  38290  rhmsubclem3  42887  rhmsubcALTVlem3  42905
  Copyright terms: Public domain W3C validator