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

Theorem anidms 568
Description: Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.)
Hypothesis
Ref Expression
anidms.1 ((𝜑𝜑) → 𝜓)
Assertion
Ref Expression
anidms (𝜑𝜓)

Proof of Theorem anidms
StepHypRef Expression
1 anidms.1 . . 3 ((𝜑𝜑) → 𝜓)
21ex 414 . 2 (𝜑 → (𝜑𝜓))
32pm2.43i 52 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  sylancb  601  sylancbr  602  eqeq12d  2754  rru  3736  dedth2v  4547  dedth3v  4548  dedth4v  4549  disjprsn  4674  opidg  4848  unisng  4885  intsng  4945  isso2i  5578  poinxp  5709  posn  5714  xpid11  5884  dfpo2  6245  predpoirr  6284  predfrirr  6285  f1oprswap  6824  f1o2sn  7083  residpr  7084  f1mpt  7203  f1eqcocnv  7242  f1eqcocnvOLD  7243  isopolem  7285  3xpexg  7677  sqxpexg  7680  poxp  8049  oe0  8436  oecl  8451  nnmsucr  8540  ecopover  8694  enrefg  8858  php  9088  phpOLD  9100  3xpfi  9197  dffi3  9301  infxpenlem  9883  isfin5  10169  isfin5-2  10261  fpwwe2lem4  10504  pwfseqlem4a  10531  pwfseqlem4  10532  pwfseqlem5  10533  pwfseq  10534  nqereu  10799  halfnq  10846  ltsopr  10902  1idsr  10968  00sr  10969  sqgt0sr  10976  leid  11185  msqgt0  11609  msqge0  11610  recextlem1  11719  recextlem2  11720  recex  11721  div1  11778  cju  12083  2halves  12315  msqznn  12519  xrltnr  12970  xrleid  13000  iccid  13239  m1expeven  13945  sqneg  13951  sqcl  13953  nnsqcl  13962  qsqcl  13964  expubnd  14010  bernneq  14059  faclbnd  14119  faclbnd3  14121  hashfac  14286  leiso  14287  cjmulval  14965  fallrisefac  15844  sin2t  15995  cos2t  15996  divalglem0  16211  divalglem2  16213  gcd0id  16335  lcmid  16421  lcmgcdeq  16424  lcmfsn  16447  isprm5  16519  prslem  18123  pslem  18397  dirref  18426  efmndbasabf  18618  efmndhash  18622  efmndbasfi  18623  efmnd1bas  18639  submefmnd  18641  sgrp2nmndlem4  18674  grpsubid  18766  grp1inv  18790  cntzi  19044  permsetexOLD  19086  symgbasfi  19095  symg1bas  19107  pgrpsubgsymg  19126  symgextfve  19136  pmtrfinv  19178  psgnsn  19237  ringadd2  19926  ipeq0  20971  matsca2  21697  matbas2  21698  matplusgcell  21710  matsubgcell  21711  mamulid  21718  mamurid  21719  mattposcl  21730  mat1dimelbas  21748  mat1dimscm  21752  mat1dimmul  21753  m1detdiag  21874  mdetdiagid  21877  mdetunilem9  21897  pmatcoe1fsupp  21978  d1mat2pmat  22016  idcn  22536  hausdiag  22924  symgtgp  23385  ustref  23498  ustelimasn  23502  iducn  23563  ismet  23604  isxmet  23605  idnghm  24035  resubmet  24093  xrsxmet  24100  cphnm  24485  tcphnmval  24521  ipcau2  24526  tcphcphlem1  24527  tcphcphlem2  24528  tcphcph  24529  cmssmscld  24642  chordthmlem  26110  slerflex  27039  ismot  27282  hmoval  29557  htth  29665  hvsubid  29773  hvnegid  29774  hv2times  29808  hiidrcl  29842  normval  29871  issh2  29956  chjidm  30267  normcan  30323  ho2times  30566  kbpj  30703  lnop0  30713  riesz3i  30809  leoprf  30875  leopsq  30876  cvnref  31038  gtiso  31416  fldextid  32138  prsss  32277  deranglem  33540  poxp2  34182  poxp3  34188  lrrecpo  34249  subsid  34339  elfix2  34420  linedegen  34659  filnetlem2  34782  bj-ru0  35344  matunitlindflem2  36006  matunitlindf  36007  ftc1anclem3  36084  prdsbnd2  36185  reheibor  36229  ismgmOLD  36240  opidon2OLD  36244  exidreslem  36267  rngo2  36297  opideq  36735  eldmcoss2  36852  2xp3dxp2ge1d  40545  sn-inelr  40836  mzpf  40961  acongrep  41206  ttac  41262  mendval  41412  iocinico  41448  iocmbl  41449  seff  42390  sblpnf  42391  sigarid  44890  cnambpcma  45317  2leaddle2  45321  clintopval  45929  2arymaptfv  46528  2arymaptfo  46531  itcoval2  46541  itcoval3  46542
  Copyright terms: Public domain W3C validator