Theorem anidms 569

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

Step	Hyp	Ref	Expression
1		anidms.1	. . 3 ⊢ ((𝜑 ∧ 𝜑) → 𝜓)
2	1	ex 415	. 2 ⊢ (𝜑 → (𝜑 → 𝜓))
3	2	pm2.43i 52	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 398

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

This theorem is referenced by:  sylancb  601  sylancbr  602  rru  3770  dedth2v  4527  dedth3v  4528  dedth4v  4529  disjprsn  4650  opidg  4822  unisng  4857  intsng  4911  snex  5332  isso2i  5508  poinxp  5632  posn  5637  xpid11  5802  predpoirr  6176  predfrirr  6177  f1oprswap  6658  f1o2sn  6904  residpr  6905  f1mpt  7019  f1eqcocnv  7057  isopolem  7098  3xpexg  7475  sqxpexg  7477  poxp  7822  oe0  8147  oecl  8162  nnmsucr  8251  ecopover  8401  enrefg  8541  php  8701  3xpfi  8790  dffi3  8895  infxpenlem  9439  isfin5  9721  isfin5-2  9813  fpwwe2lem5  10056  pwfseqlem4a  10083  pwfseqlem4  10084  pwfseqlem5  10085  pwfseq  10086  nqereu  10351  halfnq  10398  ltsopr  10454  1idsr  10520  00sr  10521  sqgt0sr  10528  leid  10736  msqgt0  11160  msqge0  11161  recextlem1  11270  recextlem2  11271  recex  11272  div1  11329  cju  11634  2halves  11866  msqznn  12065  xrltnr  12515  xrleid  12545  iccid  12784  m1expeven  13477  sqneg  13483  sqcl  13485  nnsqcl  13494  qsqcl  13496  expubnd  13542  bernneq  13591  faclbnd  13651  faclbnd3  13653  hashfac  13817  leiso  13818  cjmulval  14504  fallrisefac  15379  sin2t  15530  cos2t  15531  divalglem0  15744  divalglem2  15746  gcd0id  15867  lcmid  15953  lcmgcdeq  15956  lcmfsn  15979  isprm5  16051  prslem  17541  pslem  17816  dirref  17845  efmndbasabf  18037  efmndhash  18041  efmndbasfi  18042  efmnd1bas  18058  submefmnd  18060  sgrp2nmndlem4  18093  grpsubid  18183  grp1inv  18207  cntzi  18459  permsetex  18498  symgbasfi  18507  symg1bas  18519  pgrpsubgsymg  18537  symgextfve  18547  pmtrfinv  18589  psgnsn  18648  lsmidmOLD  18789  ringadd2  19325  ipeq0  20782  matsca2  21029  matbas2  21030  matplusgcell  21042  matsubgcell  21043  mamulid  21050  mamurid  21051  mattposcl  21062  mat1dimelbas  21080  mat1dimscm  21084  mat1dimmul  21085  m1detdiag  21206  mdetdiagid  21209  mdetunilem9  21229  pmatcoe1fsupp  21309  d1mat2pmat  21347  idcn  21865  hausdiag  22253  symgtgp  22714  ustref  22827  ustelimasn  22831  iducn  22892  ismet  22933  isxmet  22934  idnghm  23352  resubmet  23410  xrsxmet  23417  cphnm  23797  tcphnmval  23832  ipcau2  23837  tcphcphlem1  23838  tcphcphlem2  23839  tcphcph  23840  cmssmscld  23953  chordthmlem  25410  ismot  26321  hmoval  28587  htth  28695  hvsubid  28803  hvnegid  28804  hv2times  28838  hiidrcl  28872  normval  28901  issh2  28986  chjidm  29297  normcan  29353  ho2times  29596  kbpj  29733  lnop0  29743  riesz3i  29839  leoprf  29905  leopsq  29906  cvnref  30068  gtiso  30436  fldextid  31049  prsss  31159  deranglem  32413  dfpo2  32991  elfix2  33365  linedegen  33604  filnetlem2  33727  bj-ru0  34256  matunitlindflem2  34904  matunitlindf  34905  ftc1anclem3  34984  prdsbnd2  35088  reheibor  35132  ismgmOLD  35143  opidon2OLD  35147  exidreslem  35170  rngo2  35200  opideq  35615  eldmcoss2  35714  2xp3dxp2ge1d  39117  mzpf  39353  acongrep  39597  ttac  39653  mendval  39803  iocinico  39838  iocmbl  39839  seff  40661  sblpnf  40662  sigarid  43135  cnambpcma  43514  2leaddle2  43518  clintopval  44131