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  2130  eqeq12d  2747  rru  3738  dedth2v  4538  dedth3v  4539  dedth4v  4540  disjprsn  4667  opidg  4844  unisng  4877  intsng  4933  isso2i  5561  poinxp  5697  posn  5702  xpid11  5872  dfpo2  6243  predpoirr  6280  predfrirr  6281  f1oprswap  6807  f1o2sn  7075  residpr  7076  f1mpt  7195  f1eqcocnv  7235  isopolem  7279  3xpexg  7685  sqxpexg  7688  poxp  8058  poxp2  8073  poxp3  8080  oe0  8437  oecl  8452  nnmsucr  8540  ecopover  8745  enrefg  8906  php  9116  3xpfi  9205  dffi3  9315  infxpenlem  9904  isfin5  10190  isfin5-2  10282  pwfseqlem4a  10552  pwfseqlem4  10553  pwfseqlem5  10554  pwfseq  10555  nqereu  10820  halfnq  10867  ltsopr  10923  1idsr  10989  00sr  10990  sqgt0sr  10997  leid  11209  msqgt0  11637  msqge0  11638  recextlem1  11747  recextlem2  11748  recex  11749  div1  11811  cju  12121  2halves  12339  msqznn  12555  xrltnr  13018  xrleid  13050  iccid  13290  m1expeven  14016  sqneg  14022  sqcl  14025  nnsqcl  14035  qsqcl  14037  expubnd  14085  bernneq  14136  faclbnd  14197  faclbnd3  14199  hashfac  14365  leiso  14366  cjmulval  15052  fallrisefac  15932  sin2t  16086  cos2t  16087  divalglem0  16304  divalglem2  16306  gcd0id  16430  lcmid  16520  lcmgcdeq  16523  lcmfsn  16546  isprm5  16618  prslem  18203  pslem  18478  dirref  18507  efmndbasabf  18780  efmndhash  18784  efmndbasfi  18785  efmnd1bas  18801  submefmnd  18803  sgrp2nmndlem4  18836  grpsubid  18937  grp1inv  18961  cntzi  19242  symgbasfi  19292  symg1bas  19304  pgrpsubgsymg  19322  symgextfve  19332  pmtrfinv  19374  psgnsn  19433  ipeq0  21576  matsca2  22336  matbas2  22337  matplusgcell  22349  matsubgcell  22350  mamulid  22357  mamurid  22358  mattposcl  22369  mat1dimelbas  22387  mat1dimscm  22391  mat1dimmul  22392  m1detdiag  22513  mdetdiagid  22516  mdetunilem9  22536  pmatcoe1fsupp  22617  d1mat2pmat  22655  idcn  23173  hausdiag  23561  symgtgp  24022  ustref  24135  ustelimasn  24139  iducn  24198  ismet  24239  isxmet  24240  idnghm  24659  resubmet  24718  xrsxmet  24726  cphnm  25121  tcphnmval  25157  ipcau2  25162  tcphcphlem1  25163  tcphcphlem2  25164  tcphcph  25165  cmssmscld  25278  chordthmlem  26770  slerflex  27703  lrrecpo  27885  subsid  28010  divs1  28144  zsoring  28333  ismot  28514  hmoval  30788  htth  30896  hvsubid  31004  hvnegid  31005  hv2times  31039  hiidrcl  31073  normval  31102  issh2  31187  chjidm  31498  normcan  31554  ho2times  31797  kbpj  31934  lnop0  31944  riesz3i  32040  leoprf  32106  leopsq  32107  cvnref  32269  gtiso  32680  fldextid  33670  prsss  33927  fineqvnttrclse  35142  deranglem  35208  elfix2  35944  linedegen  36183  filnetlem2  36419  matunitlindflem2  37663  matunitlindf  37664  ftc1anclem3  37741  prdsbnd2  37841  reheibor  37885  ismgmOLD  37896  opidon2OLD  37900  exidreslem  37923  rngo2  37953  opideq  38377  eldmcoss2  38502  mzpf  42775  acongrep  43019  ttac  43075  mendval  43218  iocinico  43251  iocmbl  43252  seff  44348  sblpnf  44349  sigarid  46902  cnambpcma  47331  2leaddle2  47335  grlicref  48049  clintopval  48241  2arymaptfv  48689  2arymaptfo  48692  itcoval2  48702  itcoval3  48703  resipos  49012  nelsubclem  49105  initoo2  49270  termoo2  49271  setc1onsubc  49640