Theorem anidms 576

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  sylancb  611  sylancbr  612  ru0  2164  eqeq12d  2781  rru  3745  dedth2v  4546  dedth3v  4547  dedth4v  4548  disjprsn  4676  opidg  4852  unisng  4885  intsng  4943  isso2i  5596  poinxp  5732  posn  5737  xpid11  5912  dfpo2  6286  predpoirr  6323  predfrirr  6324  f1oprswap  6856  f1o2sn  7128  residpr  7129  f1mpt  7249  f1eqcocnv  7289  isopolem  7333  3xpexg  7739  sqxpexg  7742  poxp  8112  poxp2  8127  poxp3  8134  oe0  8495  oecl  8510  nnmsucr  8599  ecopover  8807  enrefg  8969  php  9179  3xpfi  9268  dffi3  9379  elirrv  9547  infxpenlem  9985  isfin5  10271  isfin5-2  10363  pwfseqlem4a  10634  pwfseqlem4  10635  pwfseqlem5  10636  pwfseq  10637  nqereu  10902  halfnq  10949  ltsopr  11005  1idsr  11071  00sr  11072  sqgt0sr  11079  leid  11294  msqgt0  11722  msqge0  11723  recextlem1  11832  recextlem2  11833  recex  11834  div1  11892  cju  12202  2halves  12450  msqznn  12666  xrltnr  13132  xrleid  13164  iccid  13405  m1expeven  14133  sqneg  14139  sqcl  14142  nnsqcl  14152  qsqcl  14154  expubnd  14202  bernneq  14253  faclbnd  14314  faclbnd3  14316  hashfac  14483  leiso  14484  cjmulval  15184  fallrisefac  16067  sin2t  16221  cos2t  16222  divalglem0  16439  divalglem2  16441  gcd0id  16565  lcmid  16655  lcmgcdeq  16658  lcmfsn  16681  isprm5  16754  prslem  18341  pslem  18616  dirref  18645  efmndbasabf  18919  efmndhash  18923  efmndbasfi  18924  efmnd1bas  18940  submefmnd  18942  sgrp2nmndlem4  18978  grpsubid  19078  grp1inv  19102  cntzi  19387  symgbasfi  19437  symg1bas  19449  pgrpsubgsymg  19467  symgextfve  19477  pmtrfinv  19519  psgnsn  19578  ipeq0  21745  matsca2  22534  matbas2  22535  matplusgcell  22547  matsubgcell  22548  mamulid  22555  mamurid  22556  mattposcl  22567  mat1dimelbas  22585  mat1dimscm  22589  mat1dimmul  22590  m1detdiag  22711  mdetdiagid  22714  mdetunilem9  22734  pmatcoe1fsupp  22815  d1mat2pmat  22853  idcn  23371  hausdiag  23759  symgtgp  24220  ustref  24333  ustelimasn  24337  iducn  24396  ismet  24437  isxmet  24438  idnghm  24857  resubmet  24916  xrsxmet  24924  cphnm  25309  tcphnmval  25345  ipcau2  25350  tcphcphlem1  25351  tcphcphlem2  25352  tcphcph  25353  cmssmscld  25466  chordthmlem  26951  lesid  27885  lrrecpo  28088  subsid  28216  divs1  28351  zsoring  28556  ismot  28758  hmoval  31067  htth  31175  hvsubid  31283  hvnegid  31284  hv2times  31318  hiidrcl  31352  normval  31381  issh2  31466  chjidm  31777  normcan  31833  ho2times  32076  kbpj  32213  lnop0  32223  riesz3i  32319  leoprf  32385  leopsq  32386  cvnref  32548  gtiso  32954  fldextid  33961  prsss  34218  fineqvnttrclse  35427  deranglem  35524  elfix2  36260  linedegen  36501  filnetlem2  36747  matunitlindflem2  38123  matunitlindf  38124  ftc1anclem3  38201  prdsbnd2  38301  reheibor  38345  ismgmOLD  38356  opidon2OLD  38360  exidreslem  38383  rngo2  38413  opideq  38849  eldmcoss2  39055  mzpf  43324  acongrep  43564  ttac  43620  mendval  43763  iocinico  43796  iocmbl  43797  seff  44878  sblpnf  44879  sigarid  47431  cnambpcma  47887  2leaddle2  47891  grlicref  48633  clintopval  48825  2arymaptfv  49283  2arymaptfo  49286  itcoval2  49296  itcoval3  49297  resipos  49605  nelsubclem  49697  initoo2  49862  termoo2  49863  setc1onsubc  50232