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

Theorem 3anidm23 1415
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 673 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  w3a 1081
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 209  df-an 399  df-3an 1083
This theorem is referenced by:  supsn  8928  infsn  8961  grusn  10218  subeq0  10904  halfaddsub  11862  avglt2  11868  modabs2  13265  efsub  15445  sinmul  15517  divalgmod  15749  modgcd  15872  pythagtriplem4  16148  pythagtriplem16  16159  pltirr  17565  latjidm  17676  latmidm  17688  ipopos  17762  mulgmodid  18258  f1omvdcnv  18564  lsmss1  18783  zntoslem  20695  obsipid  20858  smadiadetlem2  21265  smadiadet  21271  ordtt1  21979  xmet0  22944  nmsq  23790  tcphcphlem3  23828  tcphcph  23832  grpoidinvlem1  28273  grpodivid  28311  nvmid  28428  ipidsq  28479  5oalem1  29423  3oalem2  29432  unopf1o  29685  unopnorm  29686  hmopre  29692  ballotlemfc0  31738  ballotlemfcc  31739  pdivsq  32969  gcdabsorb  32972  cgr3rflx  33503  endofsegid  33534  tailini  33712  nnssi2  33791  nndivlub  33794  brin2  35639  opoccl  36312  opococ  36313  opexmid  36325  opnoncon  36326  cmtidN  36375  ltrniotaidvalN  37701  pell14qrexpclnn0  39443  rmxdbl  39516  rmydbl  39517  rhmsubclem3  44339  rhmsubcALTVlem3  44357
  Copyright terms: Public domain W3C validator