Theorem anidms 566

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 412	. 2 ⊢ (𝜑 → (𝜑 → 𝜓))
3	2	pm2.43i 52	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  sylancb  600  sylancbr  601  ru0  2127  eqeq12d  2753  rru  3785  dedth2v  4588  dedth3v  4589  dedth4v  4590  disjprsn  4714  opidg  4892  unisng  4925  intsng  4983  isso2i  5629  poinxp  5766  posn  5771  xpid11  5943  dfpo2  6316  predpoirr  6354  predfrirr  6355  f1oprswap  6892  f1o2sn  7162  residpr  7163  f1mpt  7281  f1eqcocnv  7321  isopolem  7365  3xpexg  7772  sqxpexg  7775  poxp  8153  poxp2  8168  poxp3  8175  oe0  8560  oecl  8575  nnmsucr  8663  ecopover  8861  enrefg  9024  php  9247  phpOLD  9259  3xpfi  9360  dffi3  9471  infxpenlem  10053  isfin5  10339  isfin5-2  10431  pwfseqlem4a  10701  pwfseqlem4  10702  pwfseqlem5  10703  pwfseq  10704  nqereu  10969  halfnq  11016  ltsopr  11072  1idsr  11138  00sr  11139  sqgt0sr  11146  leid  11357  msqgt0  11783  msqge0  11784  recextlem1  11893  recextlem2  11894  recex  11895  div1  11957  cju  12262  2halves  12494  msqznn  12700  xrltnr  13161  xrleid  13193  iccid  13432  m1expeven  14150  sqneg  14156  sqcl  14158  nnsqcl  14168  qsqcl  14170  expubnd  14217  bernneq  14268  faclbnd  14329  faclbnd3  14331  hashfac  14497  leiso  14498  cjmulval  15184  fallrisefac  16061  sin2t  16213  cos2t  16214  divalglem0  16430  divalglem2  16432  gcd0id  16556  lcmid  16646  lcmgcdeq  16649  lcmfsn  16672  isprm5  16744  prslem  18343  pslem  18617  dirref  18646  efmndbasabf  18885  efmndhash  18889  efmndbasfi  18890  efmnd1bas  18906  submefmnd  18908  sgrp2nmndlem4  18941  grpsubid  19042  grp1inv  19066  cntzi  19347  symgbasfi  19396  symg1bas  19408  pgrpsubgsymg  19427  symgextfve  19437  pmtrfinv  19479  psgnsn  19538  ipeq0  21656  matsca2  22426  matbas2  22427  matplusgcell  22439  matsubgcell  22440  mamulid  22447  mamurid  22448  mattposcl  22459  mat1dimelbas  22477  mat1dimscm  22481  mat1dimmul  22482  m1detdiag  22603  mdetdiagid  22606  mdetunilem9  22626  pmatcoe1fsupp  22707  d1mat2pmat  22745  idcn  23265  hausdiag  23653  symgtgp  24114  ustref  24227  ustelimasn  24231  iducn  24292  ismet  24333  isxmet  24334  idnghm  24764  resubmet  24823  xrsxmet  24831  cphnm  25227  tcphnmval  25263  ipcau2  25268  tcphcphlem1  25269  tcphcphlem2  25270  tcphcph  25271  cmssmscld  25384  chordthmlem  26875  slerflex  27808  lrrecpo  27974  subsid  28099  divs1  28229  ismot  28543  hmoval  30829  htth  30937  hvsubid  31045  hvnegid  31046  hv2times  31080  hiidrcl  31114  normval  31143  issh2  31228  chjidm  31539  normcan  31595  ho2times  31838  kbpj  31975  lnop0  31985  riesz3i  32081  leoprf  32147  leopsq  32148  cvnref  32310  gtiso  32710  fldextid  33710  prsss  33915  deranglem  35171  elfix2  35905  linedegen  36144  filnetlem2  36380  matunitlindflem2  37624  matunitlindf  37625  ftc1anclem3  37702  prdsbnd2  37802  reheibor  37846  ismgmOLD  37857  opidon2OLD  37861  exidreslem  37884  rngo2  37914  opideq  38344  eldmcoss2  38460  2xp3dxp2ge1d  42242  sn-inelr  42497  mzpf  42747  acongrep  42992  ttac  43048  mendval  43191  iocinico  43224  iocmbl  43225  seff  44328  sblpnf  44329  sigarid  46873  cnambpcma  47306  2leaddle2  47310  grlicref  47972  clintopval  48120  2arymaptfv  48572  2arymaptfo  48575  itcoval2  48585  itcoval3  48586