Theorem anidms 565

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  sylancb  598  sylancbr  599  eqeq12d  2741  rru  3772  dedth2v  4594  dedth3v  4595  dedth4v  4596  disjprsn  4722  opidg  4897  unisng  4932  intsng  4992  isso2i  5628  poinxp  5761  posn  5766  xpid11  5937  dfpo2  6306  predpoirr  6345  predfrirr  6346  f1oprswap  6886  f1o2sn  7155  residpr  7156  f1mpt  7275  f1eqcocnv  7314  isopolem  7356  3xpexg  7759  sqxpexg  7762  poxp  8141  poxp2  8156  poxp3  8163  oe0  8551  oecl  8566  nnmsucr  8654  ecopover  8849  enrefg  9014  php  9247  phpOLD  9259  3xpfi  9357  dffi3  9470  infxpenlem  10052  isfin5  10338  isfin5-2  10430  fpwwe2lem4  10673  pwfseqlem4a  10700  pwfseqlem4  10701  pwfseqlem5  10702  pwfseq  10703  nqereu  10968  halfnq  11015  ltsopr  11071  1idsr  11137  00sr  11138  sqgt0sr  11145  leid  11356  msqgt0  11780  msqge0  11781  recextlem1  11890  recextlem2  11891  recex  11892  div1  11950  cju  12255  2halves  12487  msqznn  12691  xrltnr  13148  xrleid  13179  iccid  13418  m1expeven  14124  sqneg  14130  sqcl  14132  nnsqcl  14142  qsqcl  14144  expubnd  14191  bernneq  14241  faclbnd  14302  faclbnd3  14304  hashfac  14472  leiso  14473  cjmulval  15145  fallrisefac  16022  sin2t  16174  cos2t  16175  divalglem0  16390  divalglem2  16392  gcd0id  16514  lcmid  16605  lcmgcdeq  16608  lcmfsn  16631  isprm5  16703  prslem  18318  pslem  18592  dirref  18621  efmndbasabf  18857  efmndhash  18861  efmndbasfi  18862  efmnd1bas  18878  submefmnd  18880  sgrp2nmndlem4  18913  grpsubid  19013  grp1inv  19037  cntzi  19318  permsetexOLD  19362  symgbasfi  19371  symg1bas  19383  pgrpsubgsymg  19402  symgextfve  19412  pmtrfinv  19454  psgnsn  19513  ipeq0  21626  matsca2  22405  matbas2  22406  matplusgcell  22418  matsubgcell  22419  mamulid  22426  mamurid  22427  mattposcl  22438  mat1dimelbas  22456  mat1dimscm  22460  mat1dimmul  22461  m1detdiag  22582  mdetdiagid  22585  mdetunilem9  22605  pmatcoe1fsupp  22686  d1mat2pmat  22724  idcn  23244  hausdiag  23632  symgtgp  24093  ustref  24206  ustelimasn  24210  iducn  24271  ismet  24312  isxmet  24313  idnghm  24743  resubmet  24801  xrsxmet  24808  cphnm  25204  tcphnmval  25240  ipcau2  25245  tcphcphlem1  25246  tcphcphlem2  25247  tcphcph  25248  cmssmscld  25361  chordthmlem  26852  slerflex  27785  lrrecpo  27947  subsid  28068  divs1  28196  ismot  28454  hmoval  30735  htth  30843  hvsubid  30951  hvnegid  30952  hv2times  30986  hiidrcl  31020  normval  31049  issh2  31134  chjidm  31445  normcan  31501  ho2times  31744  kbpj  31881  lnop0  31891  riesz3i  31987  leoprf  32053  leopsq  32054  cvnref  32216  gtiso  32603  fldextid  33520  prsss  33687  deranglem  34946  elfix2  35676  linedegen  35915  filnetlem2  36039  bj-ru0  36597  matunitlindflem2  37266  matunitlindf  37267  ftc1anclem3  37344  prdsbnd2  37444  reheibor  37488  ismgmOLD  37499  opidon2OLD  37503  exidreslem  37526  rngo2  37556  opideq  37989  eldmcoss2  38105  2xp3dxp2ge1d  41870  sn-inelr  42187  mzpf  42330  acongrep  42575  ttac  42631  mendval  42781  iocinico  42814  iocmbl  42815  seff  43920  sblpnf  43921  sigarid  46416  cnambpcma  46844  2leaddle2  46848  grlicref  47439  clintopval  47518  2arymaptfv  47976  2arymaptfo  47979  itcoval2  47989  itcoval3  47990