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

Theorem anidms 676
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 450 . 2 (𝜑 → (𝜑𝜓))
32pm2.43i 52 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 197  df-an 386
This theorem is referenced by:  sylancb  698  sylancbr  699  dedth2v  4121  dedth3v  4122  dedth4v  4123  disjprsn  4227  intsng  4484  pwnss  4800  snex  4879  isso2i  5037  poinxp  5153  posn  5158  xpid11  5317  predpoirr  5677  predfrirr  5678  f1oprswap  6147  f1o2sn  6373  residpr  6374  f1mpt  6483  f1eqcocnv  6521  isopolem  6560  3xpexg  6926  sqxpexg  6928  poxp  7249  oe0  7562  oecl  7577  nnmsucr  7665  ecopover  7811  ecopoverOLD  7812  enrefg  7947  php  8104  3xpfi  8192  dffi3  8297  infxpenlem  8796  xp2cda  8962  isfin5-2  9173  fpwwe2lem5  9416  pwfseqlem4a  9443  pwfseqlem4  9444  pwfseqlem5  9445  pwfseq  9446  nqereu  9711  halfnq  9758  ltsopr  9814  1idsr  9879  00sr  9880  sqgt0sr  9887  leid  10093  msqgt0  10508  msqge0  10509  recextlem1  10617  recextlem2  10618  recex  10619  div1  10676  cju  10976  2halves  11220  msqznn  11419  xrltnr  11913  xrleid  11943  iccid  12178  m1expeven  12863  expubnd  12877  sqneg  12879  sqcl  12881  nnsqcl  12889  qsqcl  12891  subsq2  12929  bernneq  12946  faclbnd  13033  faclbnd3  13035  hashfac  13196  leiso  13197  cjmulval  13835  fallrisefac  14700  sin2t  14851  cos2t  14852  divalglem0  15059  divalglem2  15061  gcd0id  15183  lcmid  15265  lcmgcdeq  15268  lcmfsn  15291  isprm5  15362  prslem  16871  pslem  17146  dirref  17175  sgrp2nmndlem4  17355  grpsubid  17439  grp1inv  17463  cntzi  17702  symgval  17739  symgbas  17740  symgbasfi  17746  symg1bas  17756  pgrpsubgsymg  17768  symgextfve  17779  pmtrfinv  17821  psgnsn  17880  lsmidm  18017  ringadd2  18515  ipeq0  19923  matsca2  20166  matbas2  20167  matplusgcell  20179  matsubgcell  20180  mamulid  20187  mamurid  20188  mattposcl  20199  mat1dimelbas  20217  mat1dimscm  20221  mat1dimmul  20222  m1detdiag  20343  mdetdiagid  20346  mdetunilem9  20366  pmatcoe1fsupp  20446  d1mat2pmat  20484  idcn  21001  hausdiag  21388  symgtgp  21845  ustref  21962  ustelimasn  21966  iducn  22027  ismet  22068  isxmet  22069  idnghm  22487  resubmet  22545  xrsxmet  22552  cphnm  22933  tchnmval  22968  ipcau2  22973  tchcphlem1  22974  tchcphlem2  22975  tchcph  22976  chordthmlem  24493  ismot  25364  hmoval  27553  htth  27663  hvsubid  27771  hvnegid  27772  hv2times  27806  hiidrcl  27840  normval  27869  issh2  27954  chjidm  28267  normcan  28323  ho2times  28566  kbpj  28703  lnop0  28713  riesz3i  28809  leoprf  28875  leopsq  28876  cvnref  29038  gtiso  29362  prsss  29786  deranglem  30909  dfpo2  31406  elfix2  31706  linedegen  31945  filnetlem2  32069  bj-ru0  32632  matunitlindflem2  33077  matunitlindf  33078  ftc1anclem3  33158  prdsbnd2  33265  reheibor  33309  ismgmOLD  33320  opidon2OLD  33324  exidreslem  33347  rngo2  33377  mzpf  36818  acongrep  37066  ttac  37122  mendval  37273  mendplusgfval  37275  mendmulrfval  37277  iocinico  37317  iocmbl  37318  seff  38029  sblpnf  38030  sigarid  40381  opidg  40624  cnambpcma  40636  2leaddle2  40639  clintopval  41158
  Copyright terms: Public domain W3C validator