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  3750  dedth2v  4551  dedth3v  4552  dedth4v  4553  disjprsn  4678  opidg  4856  unisng  4889  intsng  4947  isso2i  5583  poinxp  5719  posn  5724  xpid11  5896  dfpo2  6269  predpoirr  6306  predfrirr  6307  f1oprswap  6844  f1o2sn  7114  residpr  7115  f1mpt  7236  f1eqcocnv  7276  isopolem  7320  3xpexg  7728  sqxpexg  7731  poxp  8107  poxp2  8122  poxp3  8129  oe0  8486  oecl  8501  nnmsucr  8589  ecopover  8794  enrefg  8955  php  9171  3xpfi  9271  dffi3  9382  infxpenlem  9966  isfin5  10252  isfin5-2  10344  pwfseqlem4a  10614  pwfseqlem4  10615  pwfseqlem5  10616  pwfseq  10617  nqereu  10882  halfnq  10929  ltsopr  10985  1idsr  11051  00sr  11052  sqgt0sr  11059  leid  11270  msqgt0  11698  msqge0  11699  recextlem1  11808  recextlem2  11809  recex  11810  div1  11872  cju  12182  2halves  12400  msqznn  12616  xrltnr  13079  xrleid  13111  iccid  13351  m1expeven  14074  sqneg  14080  sqcl  14083  nnsqcl  14093  qsqcl  14095  expubnd  14143  bernneq  14194  faclbnd  14255  faclbnd3  14257  hashfac  14423  leiso  14424  cjmulval  15111  fallrisefac  15991  sin2t  16145  cos2t  16146  divalglem0  16363  divalglem2  16365  gcd0id  16489  lcmid  16579  lcmgcdeq  16582  lcmfsn  16605  isprm5  16677  prslem  18258  pslem  18531  dirref  18560  efmndbasabf  18799  efmndhash  18803  efmndbasfi  18804  efmnd1bas  18820  submefmnd  18822  sgrp2nmndlem4  18855  grpsubid  18956  grp1inv  18980  cntzi  19261  symgbasfi  19309  symg1bas  19321  pgrpsubgsymg  19339  symgextfve  19349  pmtrfinv  19391  psgnsn  19450  ipeq0  21547  matsca2  22307  matbas2  22308  matplusgcell  22320  matsubgcell  22321  mamulid  22328  mamurid  22329  mattposcl  22340  mat1dimelbas  22358  mat1dimscm  22362  mat1dimmul  22363  m1detdiag  22484  mdetdiagid  22487  mdetunilem9  22507  pmatcoe1fsupp  22588  d1mat2pmat  22626  idcn  23144  hausdiag  23532  symgtgp  23993  ustref  24106  ustelimasn  24110  iducn  24170  ismet  24211  isxmet  24212  idnghm  24631  resubmet  24690  xrsxmet  24698  cphnm  25093  tcphnmval  25129  ipcau2  25134  tcphcphlem1  25135  tcphcphlem2  25136  tcphcph  25137  cmssmscld  25250  chordthmlem  26742  slerflex  27675  lrrecpo  27848  subsid  27973  divs1  28107  ismot  28462  hmoval  30739  htth  30847  hvsubid  30955  hvnegid  30956  hv2times  30990  hiidrcl  31024  normval  31053  issh2  31138  chjidm  31449  normcan  31505  ho2times  31748  kbpj  31885  lnop0  31895  riesz3i  31991  leoprf  32057  leopsq  32058  cvnref  32220  gtiso  32624  fldextid  33655  prsss  33906  deranglem  35153  elfix2  35892  linedegen  36131  filnetlem2  36367  matunitlindflem2  37611  matunitlindf  37612  ftc1anclem3  37689  prdsbnd2  37789  reheibor  37833  ismgmOLD  37844  opidon2OLD  37848  exidreslem  37871  rngo2  37901  opideq  38325  eldmcoss2  38450  mzpf  42724  acongrep  42969  ttac  43025  mendval  43168  iocinico  43201  iocmbl  43202  seff  44298  sblpnf  44299  sigarid  46856  cnambpcma  47295  2leaddle2  47299  grlicref  48004  clintopval  48192  2arymaptfv  48640  2arymaptfo  48643  itcoval2  48653  itcoval3  48654  resipos  48963  nelsubclem  49056  initoo2  49221  termoo2  49222  setc1onsubc  49591