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  2749  rru  3741  dedth2v  4552  dedth3v  4553  dedth4v  4554  disjprsn  4679  opidg  4853  unisng  4890  intsng  4950  isso2i  5584  poinxp  5716  posn  5721  xpid11  5891  dfpo2  6252  predpoirr  6291  predfrirr  6292  f1oprswap  6832  f1o2sn  7092  residpr  7093  f1mpt  7212  f1eqcocnv  7251  f1eqcocnvOLD  7252  isopolem  7294  3xpexg  7690  sqxpexg  7693  poxp  8064  poxp2  8079  poxp3  8086  oe0  8472  oecl  8487  nnmsucr  8576  ecopover  8766  enrefg  8930  php  9160  phpOLD  9172  3xpfi  9269  dffi3  9375  infxpenlem  9957  isfin5  10243  isfin5-2  10335  fpwwe2lem4  10578  pwfseqlem4a  10605  pwfseqlem4  10606  pwfseqlem5  10607  pwfseq  10608  nqereu  10873  halfnq  10920  ltsopr  10976  1idsr  11042  00sr  11043  sqgt0sr  11050  leid  11259  msqgt0  11683  msqge0  11684  recextlem1  11793  recextlem2  11794  recex  11795  div1  11852  cju  12157  2halves  12389  msqznn  12593  xrltnr  13048  xrleid  13079  iccid  13318  m1expeven  14024  sqneg  14030  sqcl  14032  nnsqcl  14042  qsqcl  14044  expubnd  14091  bernneq  14141  faclbnd  14199  faclbnd3  14201  hashfac  14366  leiso  14367  cjmulval  15039  fallrisefac  15916  sin2t  16067  cos2t  16068  divalglem0  16283  divalglem2  16285  gcd0id  16407  lcmid  16493  lcmgcdeq  16496  lcmfsn  16519  isprm5  16591  prslem  18195  pslem  18469  dirref  18498  efmndbasabf  18690  efmndhash  18694  efmndbasfi  18695  efmnd1bas  18711  submefmnd  18713  sgrp2nmndlem4  18746  grpsubid  18839  grp1inv  18863  cntzi  19117  permsetexOLD  19159  symgbasfi  19168  symg1bas  19180  pgrpsubgsymg  19199  symgextfve  19209  pmtrfinv  19251  psgnsn  19310  ipeq0  21065  matsca2  21792  matbas2  21793  matplusgcell  21805  matsubgcell  21806  mamulid  21813  mamurid  21814  mattposcl  21825  mat1dimelbas  21843  mat1dimscm  21847  mat1dimmul  21848  m1detdiag  21969  mdetdiagid  21972  mdetunilem9  21992  pmatcoe1fsupp  22073  d1mat2pmat  22111  idcn  22631  hausdiag  23019  symgtgp  23480  ustref  23593  ustelimasn  23597  iducn  23658  ismet  23699  isxmet  23700  idnghm  24130  resubmet  24188  xrsxmet  24195  cphnm  24580  tcphnmval  24616  ipcau2  24621  tcphcphlem1  24622  tcphcphlem2  24623  tcphcph  24624  cmssmscld  24737  chordthmlem  26205  slerflex  27134  lrrecpo  27282  subsid  27385  ismot  27526  hmoval  29801  htth  29909  hvsubid  30017  hvnegid  30018  hv2times  30052  hiidrcl  30086  normval  30115  issh2  30200  chjidm  30511  normcan  30567  ho2times  30810  kbpj  30947  lnop0  30957  riesz3i  31053  leoprf  31119  leopsq  31120  cvnref  31282  gtiso  31668  fldextid  32412  prsss  32561  deranglem  33824  elfix2  34542  linedegen  34781  filnetlem2  34904  bj-ru0  35463  matunitlindflem2  36125  matunitlindf  36126  ftc1anclem3  36203  prdsbnd2  36304  reheibor  36348  ismgmOLD  36359  opidon2OLD  36363  exidreslem  36386  rngo2  36416  opideq  36854  eldmcoss2  36971  2xp3dxp2ge1d  40664  sn-inelr  40981  mzpf  41106  acongrep  41351  ttac  41407  mendval  41557  iocinico  41593  iocmbl  41594  seff  42681  sblpnf  42682  sigarid  45189  cnambpcma  45616  2leaddle2  45620  clintopval  46228  2arymaptfv  46827  2arymaptfo  46830  itcoval2  46840  itcoval3  46841
  Copyright terms: Public domain W3C validator