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  2751  rru  3762  dedth2v  4563  dedth3v  4564  dedth4v  4565  disjprsn  4690  opidg  4868  unisng  4901  intsng  4959  isso2i  5598  poinxp  5735  posn  5740  xpid11  5912  dfpo2  6285  predpoirr  6322  predfrirr  6323  f1oprswap  6861  f1o2sn  7131  residpr  7132  f1mpt  7253  f1eqcocnv  7293  isopolem  7337  3xpexg  7744  sqxpexg  7747  poxp  8125  poxp2  8140  poxp3  8147  oe0  8532  oecl  8547  nnmsucr  8635  ecopover  8833  enrefg  8996  php  9219  phpOLD  9229  3xpfi  9330  dffi3  9441  infxpenlem  10025  isfin5  10311  isfin5-2  10403  pwfseqlem4a  10673  pwfseqlem4  10674  pwfseqlem5  10675  pwfseq  10676  nqereu  10941  halfnq  10988  ltsopr  11044  1idsr  11110  00sr  11111  sqgt0sr  11118  leid  11329  msqgt0  11755  msqge0  11756  recextlem1  11865  recextlem2  11866  recex  11867  div1  11929  cju  12234  2halves  12457  msqznn  12673  xrltnr  13133  xrleid  13165  iccid  13405  m1expeven  14125  sqneg  14131  sqcl  14134  nnsqcl  14144  qsqcl  14146  expubnd  14194  bernneq  14245  faclbnd  14306  faclbnd3  14308  hashfac  14474  leiso  14475  cjmulval  15162  fallrisefac  16039  sin2t  16193  cos2t  16194  divalglem0  16410  divalglem2  16412  gcd0id  16536  lcmid  16626  lcmgcdeq  16629  lcmfsn  16652  isprm5  16724  prslem  18307  pslem  18580  dirref  18609  efmndbasabf  18848  efmndhash  18852  efmndbasfi  18853  efmnd1bas  18869  submefmnd  18871  sgrp2nmndlem4  18904  grpsubid  19005  grp1inv  19029  cntzi  19310  symgbasfi  19358  symg1bas  19370  pgrpsubgsymg  19388  symgextfve  19398  pmtrfinv  19440  psgnsn  19499  ipeq0  21596  matsca2  22356  matbas2  22357  matplusgcell  22369  matsubgcell  22370  mamulid  22377  mamurid  22378  mattposcl  22389  mat1dimelbas  22407  mat1dimscm  22411  mat1dimmul  22412  m1detdiag  22533  mdetdiagid  22536  mdetunilem9  22556  pmatcoe1fsupp  22637  d1mat2pmat  22675  idcn  23193  hausdiag  23581  symgtgp  24042  ustref  24155  ustelimasn  24159  iducn  24219  ismet  24260  isxmet  24261  idnghm  24680  resubmet  24739  xrsxmet  24747  cphnm  25143  tcphnmval  25179  ipcau2  25184  tcphcphlem1  25185  tcphcphlem2  25186  tcphcph  25187  cmssmscld  25300  chordthmlem  26792  slerflex  27725  lrrecpo  27891  subsid  28016  divs1  28146  ismot  28460  hmoval  30737  htth  30845  hvsubid  30953  hvnegid  30954  hv2times  30988  hiidrcl  31022  normval  31051  issh2  31136  chjidm  31447  normcan  31503  ho2times  31746  kbpj  31883  lnop0  31893  riesz3i  31989  leoprf  32055  leopsq  32056  cvnref  32218  gtiso  32624  fldextid  33647  prsss  33893  deranglem  35134  elfix2  35868  linedegen  36107  filnetlem2  36343  matunitlindflem2  37587  matunitlindf  37588  ftc1anclem3  37665  prdsbnd2  37765  reheibor  37809  ismgmOLD  37820  opidon2OLD  37824  exidreslem  37847  rngo2  37877  opideq  38307  eldmcoss2  38423  2xp3dxp2ge1d  42200  sn-inelr  42457  mzpf  42706  acongrep  42951  ttac  43007  mendval  43150  iocinico  43183  iocmbl  43184  seff  44281  sblpnf  44282  sigarid  46835  cnambpcma  47271  2leaddle2  47275  grlicref  47965  clintopval  48127  2arymaptfv  48579  2arymaptfo  48582  itcoval2  48592  itcoval3  48593  resipos  48897  nelsubclem  48982  initoo2  49066  termoo2  49067  setc1onsubc  49394