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  2128  eqeq12d  2745  rru  3741  dedth2v  4541  dedth3v  4542  dedth4v  4543  disjprsn  4668  opidg  4846  unisng  4879  intsng  4936  isso2i  5568  poinxp  5704  posn  5709  xpid11  5878  dfpo2  6248  predpoirr  6285  predfrirr  6286  f1oprswap  6812  f1o2sn  7080  residpr  7081  f1mpt  7202  f1eqcocnv  7242  isopolem  7286  3xpexg  7692  sqxpexg  7695  poxp  8068  poxp2  8083  poxp3  8090  oe0  8447  oecl  8462  nnmsucr  8550  ecopover  8755  enrefg  8916  php  9131  3xpfi  9229  dffi3  9340  infxpenlem  9926  isfin5  10212  isfin5-2  10304  pwfseqlem4a  10574  pwfseqlem4  10575  pwfseqlem5  10576  pwfseq  10577  nqereu  10842  halfnq  10889  ltsopr  10945  1idsr  11011  00sr  11012  sqgt0sr  11019  leid  11230  msqgt0  11658  msqge0  11659  recextlem1  11768  recextlem2  11769  recex  11770  div1  11832  cju  12142  2halves  12360  msqznn  12576  xrltnr  13039  xrleid  13071  iccid  13311  m1expeven  14034  sqneg  14040  sqcl  14043  nnsqcl  14053  qsqcl  14055  expubnd  14103  bernneq  14154  faclbnd  14215  faclbnd3  14217  hashfac  14383  leiso  14384  cjmulval  15070  fallrisefac  15950  sin2t  16104  cos2t  16105  divalglem0  16322  divalglem2  16324  gcd0id  16448  lcmid  16538  lcmgcdeq  16541  lcmfsn  16564  isprm5  16636  prslem  18221  pslem  18496  dirref  18525  efmndbasabf  18764  efmndhash  18768  efmndbasfi  18769  efmnd1bas  18785  submefmnd  18787  sgrp2nmndlem4  18820  grpsubid  18921  grp1inv  18945  cntzi  19226  symgbasfi  19276  symg1bas  19288  pgrpsubgsymg  19306  symgextfve  19316  pmtrfinv  19358  psgnsn  19417  ipeq0  21563  matsca2  22323  matbas2  22324  matplusgcell  22336  matsubgcell  22337  mamulid  22344  mamurid  22345  mattposcl  22356  mat1dimelbas  22374  mat1dimscm  22378  mat1dimmul  22379  m1detdiag  22500  mdetdiagid  22503  mdetunilem9  22523  pmatcoe1fsupp  22604  d1mat2pmat  22642  idcn  23160  hausdiag  23548  symgtgp  24009  ustref  24122  ustelimasn  24126  iducn  24186  ismet  24227  isxmet  24228  idnghm  24647  resubmet  24706  xrsxmet  24714  cphnm  25109  tcphnmval  25145  ipcau2  25150  tcphcphlem1  25151  tcphcphlem2  25152  tcphcph  25153  cmssmscld  25266  chordthmlem  26758  slerflex  27691  lrrecpo  27871  subsid  27996  divs1  28130  zsoring  28319  ismot  28498  hmoval  30772  htth  30880  hvsubid  30988  hvnegid  30989  hv2times  31023  hiidrcl  31057  normval  31086  issh2  31171  chjidm  31482  normcan  31538  ho2times  31781  kbpj  31918  lnop0  31928  riesz3i  32024  leoprf  32090  leopsq  32091  cvnref  32253  gtiso  32657  fldextid  33634  prsss  33885  deranglem  35141  elfix2  35880  linedegen  36119  filnetlem2  36355  matunitlindflem2  37599  matunitlindf  37600  ftc1anclem3  37677  prdsbnd2  37777  reheibor  37821  ismgmOLD  37832  opidon2OLD  37836  exidreslem  37859  rngo2  37889  opideq  38313  eldmcoss2  38438  mzpf  42712  acongrep  42956  ttac  43012  mendval  43155  iocinico  43188  iocmbl  43189  seff  44285  sblpnf  44286  sigarid  46843  cnambpcma  47282  2leaddle2  47286  grlicref  48000  clintopval  48192  2arymaptfv  48640  2arymaptfo  48643  itcoval2  48653  itcoval3  48654  resipos  48963  nelsubclem  49056  initoo2  49221  termoo2  49222  setc1onsubc  49591