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  2124  eqeq12d  2750  rru  3787  dedth2v  4592  dedth3v  4593  dedth4v  4594  disjprsn  4718  opidg  4896  unisng  4929  intsng  4987  isso2i  5632  poinxp  5768  posn  5773  xpid11  5945  dfpo2  6317  predpoirr  6355  predfrirr  6356  f1oprswap  6892  f1o2sn  7161  residpr  7162  f1mpt  7280  f1eqcocnv  7320  isopolem  7364  3xpexg  7770  sqxpexg  7773  poxp  8151  poxp2  8166  poxp3  8173  oe0  8558  oecl  8573  nnmsucr  8661  ecopover  8859  enrefg  9022  php  9244  phpOLD  9256  3xpfi  9357  dffi3  9468  infxpenlem  10050  isfin5  10336  isfin5-2  10428  pwfseqlem4a  10698  pwfseqlem4  10699  pwfseqlem5  10700  pwfseq  10701  nqereu  10966  halfnq  11013  ltsopr  11069  1idsr  11135  00sr  11136  sqgt0sr  11143  leid  11354  msqgt0  11780  msqge0  11781  recextlem1  11890  recextlem2  11891  recex  11892  div1  11954  cju  12259  2halves  12491  msqznn  12697  xrltnr  13158  xrleid  13189  iccid  13428  m1expeven  14146  sqneg  14152  sqcl  14154  nnsqcl  14164  qsqcl  14166  expubnd  14213  bernneq  14264  faclbnd  14325  faclbnd3  14327  hashfac  14493  leiso  14494  cjmulval  15180  fallrisefac  16057  sin2t  16209  cos2t  16210  divalglem0  16426  divalglem2  16428  gcd0id  16552  lcmid  16642  lcmgcdeq  16645  lcmfsn  16668  isprm5  16740  prslem  18354  pslem  18629  dirref  18658  efmndbasabf  18897  efmndhash  18901  efmndbasfi  18902  efmnd1bas  18918  submefmnd  18920  sgrp2nmndlem4  18953  grpsubid  19054  grp1inv  19078  cntzi  19359  symgbasfi  19410  symg1bas  19422  pgrpsubgsymg  19441  symgextfve  19451  pmtrfinv  19493  psgnsn  19552  ipeq0  21673  matsca2  22441  matbas2  22442  matplusgcell  22454  matsubgcell  22455  mamulid  22462  mamurid  22463  mattposcl  22474  mat1dimelbas  22492  mat1dimscm  22496  mat1dimmul  22497  m1detdiag  22618  mdetdiagid  22621  mdetunilem9  22641  pmatcoe1fsupp  22722  d1mat2pmat  22760  idcn  23280  hausdiag  23668  symgtgp  24129  ustref  24242  ustelimasn  24246  iducn  24307  ismet  24348  isxmet  24349  idnghm  24779  resubmet  24837  xrsxmet  24844  cphnm  25240  tcphnmval  25276  ipcau2  25281  tcphcphlem1  25282  tcphcphlem2  25283  tcphcph  25284  cmssmscld  25397  chordthmlem  26889  slerflex  27822  lrrecpo  27988  subsid  28113  divs1  28243  ismot  28557  hmoval  30838  htth  30946  hvsubid  31054  hvnegid  31055  hv2times  31089  hiidrcl  31123  normval  31152  issh2  31237  chjidm  31548  normcan  31604  ho2times  31847  kbpj  31984  lnop0  31994  riesz3i  32090  leoprf  32156  leopsq  32157  cvnref  32319  gtiso  32715  fldextid  33686  prsss  33876  deranglem  35150  elfix2  35885  linedegen  36124  filnetlem2  36361  matunitlindflem2  37603  matunitlindf  37604  ftc1anclem3  37681  prdsbnd2  37781  reheibor  37825  ismgmOLD  37836  opidon2OLD  37840  exidreslem  37863  rngo2  37893  opideq  38324  eldmcoss2  38440  2xp3dxp2ge1d  42222  sn-inelr  42473  mzpf  42723  acongrep  42968  ttac  43024  mendval  43167  iocinico  43200  iocmbl  43201  seff  44304  sblpnf  44305  sigarid  46813  cnambpcma  47243  2leaddle2  47247  grlicref  47907  clintopval  48047  2arymaptfv  48500  2arymaptfo  48503  itcoval2  48513  itcoval3  48514