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  3747  dedth2v  4547  dedth3v  4548  dedth4v  4549  disjprsn  4674  opidg  4852  unisng  4885  intsng  4943  isso2i  5576  poinxp  5712  posn  5717  xpid11  5885  dfpo2  6257  predpoirr  6294  predfrirr  6295  f1oprswap  6826  f1o2sn  7096  residpr  7097  f1mpt  7218  f1eqcocnv  7258  isopolem  7302  3xpexg  7708  sqxpexg  7711  poxp  8084  poxp2  8099  poxp3  8106  oe0  8463  oecl  8478  nnmsucr  8566  ecopover  8771  enrefg  8932  php  9148  3xpfi  9247  dffi3  9358  infxpenlem  9942  isfin5  10228  isfin5-2  10320  pwfseqlem4a  10590  pwfseqlem4  10591  pwfseqlem5  10592  pwfseq  10593  nqereu  10858  halfnq  10905  ltsopr  10961  1idsr  11027  00sr  11028  sqgt0sr  11035  leid  11246  msqgt0  11674  msqge0  11675  recextlem1  11784  recextlem2  11785  recex  11786  div1  11848  cju  12158  2halves  12376  msqznn  12592  xrltnr  13055  xrleid  13087  iccid  13327  m1expeven  14050  sqneg  14056  sqcl  14059  nnsqcl  14069  qsqcl  14071  expubnd  14119  bernneq  14170  faclbnd  14231  faclbnd3  14233  hashfac  14399  leiso  14400  cjmulval  15087  fallrisefac  15967  sin2t  16121  cos2t  16122  divalglem0  16339  divalglem2  16341  gcd0id  16465  lcmid  16555  lcmgcdeq  16558  lcmfsn  16581  isprm5  16653  prslem  18234  pslem  18507  dirref  18536  efmndbasabf  18775  efmndhash  18779  efmndbasfi  18780  efmnd1bas  18796  submefmnd  18798  sgrp2nmndlem4  18831  grpsubid  18932  grp1inv  18956  cntzi  19237  symgbasfi  19285  symg1bas  19297  pgrpsubgsymg  19315  symgextfve  19325  pmtrfinv  19367  psgnsn  19426  ipeq0  21523  matsca2  22283  matbas2  22284  matplusgcell  22296  matsubgcell  22297  mamulid  22304  mamurid  22305  mattposcl  22316  mat1dimelbas  22334  mat1dimscm  22338  mat1dimmul  22339  m1detdiag  22460  mdetdiagid  22463  mdetunilem9  22483  pmatcoe1fsupp  22564  d1mat2pmat  22602  idcn  23120  hausdiag  23508  symgtgp  23969  ustref  24082  ustelimasn  24086  iducn  24146  ismet  24187  isxmet  24188  idnghm  24607  resubmet  24666  xrsxmet  24674  cphnm  25069  tcphnmval  25105  ipcau2  25110  tcphcphlem1  25111  tcphcphlem2  25112  tcphcph  25113  cmssmscld  25226  chordthmlem  26718  slerflex  27651  lrrecpo  27824  subsid  27949  divs1  28083  ismot  28438  hmoval  30712  htth  30820  hvsubid  30928  hvnegid  30929  hv2times  30963  hiidrcl  30997  normval  31026  issh2  31111  chjidm  31422  normcan  31478  ho2times  31721  kbpj  31858  lnop0  31868  riesz3i  31964  leoprf  32030  leopsq  32031  cvnref  32193  gtiso  32597  fldextid  33628  prsss  33879  deranglem  35126  elfix2  35865  linedegen  36104  filnetlem2  36340  matunitlindflem2  37584  matunitlindf  37585  ftc1anclem3  37662  prdsbnd2  37762  reheibor  37806  ismgmOLD  37817  opidon2OLD  37821  exidreslem  37844  rngo2  37874  opideq  38298  eldmcoss2  38423  mzpf  42697  acongrep  42942  ttac  42998  mendval  43141  iocinico  43174  iocmbl  43175  seff  44271  sblpnf  44272  sigarid  46829  cnambpcma  47268  2leaddle2  47272  grlicref  47977  clintopval  48165  2arymaptfv  48613  2arymaptfo  48616  itcoval2  48626  itcoval3  48627  resipos  48936  nelsubclem  49029  initoo2  49194  termoo2  49195  setc1onsubc  49564