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

Theorem 3anidm23 1423
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 1119 . 2 (((𝜑𝜓) ∧ 𝜓) → 𝜒)
32anabss3 675 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087
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 207  df-an 396  df-3an 1089
This theorem is referenced by:  supsn  9512  infsn  9545  grusn  10844  subeq0  11535  halfaddsub  12499  avglt2  12505  modabs2  13945  efsub  16136  sinmul  16208  divalgmod  16443  modgcd  16569  pythagtriplem4  16857  pythagtriplem16  16868  pltirr  18380  latjidm  18507  latmidm  18519  ipopos  18581  mulgmodid  19131  f1omvdcnv  19462  lsmss1  19683  rhmsubclem3  20687  zntoslem  21575  obsipid  21742  smadiadetlem2  22670  smadiadet  22676  ordtt1  23387  xmet0  24352  nmsq  25228  tcphcphlem3  25267  tcphcph  25271  grpoidinvlem1  30523  grpodivid  30561  nvmid  30678  ipidsq  30729  5oalem1  31673  3oalem2  31682  unopf1o  31935  unopnorm  31936  hmopre  31942  ballotlemfc0  34495  ballotlemfcc  34496  gcdabsorb  35750  cgr3rflx  36055  endofsegid  36086  tailini  36377  nnssi2  36456  nndivlub  36459  brin2  38410  opoccl  39195  opococ  39196  opexmid  39208  opnoncon  39209  cmtidN  39258  ltrniotaidvalN  40585  pell14qrexpclnn0  42877  rmxdbl  42951  rmydbl  42952  rhmsubcALTVlem3  48199
  Copyright terms: Public domain W3C validator