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  599  sylancbr  600  ru0  2127  eqeq12d  2756  rru  3801  dedth2v  4610  dedth3v  4611  dedth4v  4612  disjprsn  4739  opidg  4916  unisng  4949  intsng  5007  isso2i  5644  poinxp  5780  posn  5785  xpid11  5957  dfpo2  6327  predpoirr  6365  predfrirr  6366  f1oprswap  6906  f1o2sn  7176  residpr  7177  f1mpt  7298  f1eqcocnv  7337  isopolem  7381  3xpexg  7787  sqxpexg  7790  poxp  8169  poxp2  8184  poxp3  8191  oe0  8578  oecl  8593  nnmsucr  8681  ecopover  8879  enrefg  9044  php  9273  phpOLD  9285  3xpfi  9388  dffi3  9500  infxpenlem  10082  isfin5  10368  isfin5-2  10460  pwfseqlem4a  10730  pwfseqlem4  10731  pwfseqlem5  10732  pwfseq  10733  nqereu  10998  halfnq  11045  ltsopr  11101  1idsr  11167  00sr  11168  sqgt0sr  11175  leid  11386  msqgt0  11810  msqge0  11811  recextlem1  11920  recextlem2  11921  recex  11922  div1  11984  cju  12289  2halves  12521  msqznn  12725  xrltnr  13182  xrleid  13213  iccid  13452  m1expeven  14160  sqneg  14166  sqcl  14168  nnsqcl  14178  qsqcl  14180  expubnd  14227  bernneq  14278  faclbnd  14339  faclbnd3  14341  hashfac  14507  leiso  14508  cjmulval  15194  fallrisefac  16073  sin2t  16225  cos2t  16226  divalglem0  16441  divalglem2  16443  gcd0id  16565  lcmid  16656  lcmgcdeq  16659  lcmfsn  16682  isprm5  16754  prslem  18368  pslem  18642  dirref  18671  efmndbasabf  18907  efmndhash  18911  efmndbasfi  18912  efmnd1bas  18928  submefmnd  18930  sgrp2nmndlem4  18963  grpsubid  19064  grp1inv  19088  cntzi  19369  symgbasfi  19420  symg1bas  19432  pgrpsubgsymg  19451  symgextfve  19461  pmtrfinv  19503  psgnsn  19562  ipeq0  21679  matsca2  22447  matbas2  22448  matplusgcell  22460  matsubgcell  22461  mamulid  22468  mamurid  22469  mattposcl  22480  mat1dimelbas  22498  mat1dimscm  22502  mat1dimmul  22503  m1detdiag  22624  mdetdiagid  22627  mdetunilem9  22647  pmatcoe1fsupp  22728  d1mat2pmat  22766  idcn  23286  hausdiag  23674  symgtgp  24135  ustref  24248  ustelimasn  24252  iducn  24313  ismet  24354  isxmet  24355  idnghm  24785  resubmet  24843  xrsxmet  24850  cphnm  25246  tcphnmval  25282  ipcau2  25287  tcphcphlem1  25288  tcphcphlem2  25289  tcphcph  25290  cmssmscld  25403  chordthmlem  26893  slerflex  27826  lrrecpo  27992  subsid  28117  divs1  28247  ismot  28561  hmoval  30842  htth  30950  hvsubid  31058  hvnegid  31059  hv2times  31093  hiidrcl  31127  normval  31156  issh2  31241  chjidm  31552  normcan  31608  ho2times  31851  kbpj  31988  lnop0  31998  riesz3i  32094  leoprf  32160  leopsq  32161  cvnref  32323  gtiso  32712  fldextid  33672  prsss  33862  deranglem  35134  elfix2  35868  linedegen  36107  filnetlem2  36345  matunitlindflem2  37577  matunitlindf  37578  ftc1anclem3  37655  prdsbnd2  37755  reheibor  37799  ismgmOLD  37810  opidon2OLD  37814  exidreslem  37837  rngo2  37867  opideq  38299  eldmcoss2  38415  2xp3dxp2ge1d  42198  sn-inelr  42443  mzpf  42692  acongrep  42937  ttac  42993  mendval  43140  iocinico  43173  iocmbl  43174  seff  44278  sblpnf  44279  sigarid  46779  cnambpcma  47209  2leaddle2  47213  grlicref  47829  clintopval  47927  2arymaptfv  48385  2arymaptfo  48388  itcoval2  48398  itcoval3  48399