Theorem anidms 567

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  sylancb  600  sylancbr  601  eqeq12d  2755  rru  3715  dedth2v  4522  dedth3v  4523  dedth4v  4524  disjprsn  4651  opidg  4824  unisng  4861  intsng  4917  snex  5355  isso2i  5539  poinxp  5668  posn  5673  xpid11  5844  dfpo2  6203  predpoirr  6240  predfrirr  6241  f1oprswap  6769  f1o2sn  7023  residpr  7024  f1mpt  7143  f1eqcocnv  7182  f1eqcocnvOLD  7183  isopolem  7225  3xpexg  7611  sqxpexg  7614  poxp  7978  oe0  8361  oecl  8376  nnmsucr  8465  ecopover  8619  enrefg  8781  php  9002  phpOLD  9014  3xpfi  9095  dffi3  9199  infxpenlem  9778  isfin5  10064  isfin5-2  10156  fpwwe2lem4  10399  pwfseqlem4a  10426  pwfseqlem4  10427  pwfseqlem5  10428  pwfseq  10429  nqereu  10694  halfnq  10741  ltsopr  10797  1idsr  10863  00sr  10864  sqgt0sr  10871  leid  11080  msqgt0  11504  msqge0  11505  recextlem1  11614  recextlem2  11615  recex  11616  div1  11673  cju  11978  2halves  12210  msqznn  12411  xrltnr  12864  xrleid  12894  iccid  13133  m1expeven  13839  sqneg  13845  sqcl  13847  nnsqcl  13856  qsqcl  13858  expubnd  13904  bernneq  13953  faclbnd  14013  faclbnd3  14015  hashfac  14181  leiso  14182  cjmulval  14865  fallrisefac  15744  sin2t  15895  cos2t  15896  divalglem0  16111  divalglem2  16113  gcd0id  16235  lcmid  16323  lcmgcdeq  16326  lcmfsn  16349  isprm5  16421  prslem  18025  pslem  18299  dirref  18328  efmndbasabf  18520  efmndhash  18524  efmndbasfi  18525  efmnd1bas  18541  submefmnd  18543  sgrp2nmndlem4  18576  grpsubid  18668  grp1inv  18692  cntzi  18944  permsetexOLD  18986  symgbasfi  18995  symg1bas  19007  pgrpsubgsymg  19026  symgextfve  19036  pmtrfinv  19078  psgnsn  19137  lsmidmOLD  19278  ringadd2  19823  ipeq0  20852  matsca2  21578  matbas2  21579  matplusgcell  21591  matsubgcell  21592  mamulid  21599  mamurid  21600  mattposcl  21611  mat1dimelbas  21629  mat1dimscm  21633  mat1dimmul  21634  m1detdiag  21755  mdetdiagid  21758  mdetunilem9  21778  pmatcoe1fsupp  21859  d1mat2pmat  21897  idcn  22417  hausdiag  22805  symgtgp  23266  ustref  23379  ustelimasn  23383  iducn  23444  ismet  23485  isxmet  23486  idnghm  23916  resubmet  23974  xrsxmet  23981  cphnm  24366  tcphnmval  24402  ipcau2  24407  tcphcphlem1  24408  tcphcphlem2  24409  tcphcph  24410  cmssmscld  24523  chordthmlem  25991  ismot  26905  hmoval  29181  htth  29289  hvsubid  29397  hvnegid  29398  hv2times  29432  hiidrcl  29466  normval  29495  issh2  29580  chjidm  29891  normcan  29947  ho2times  30190  kbpj  30327  lnop0  30337  riesz3i  30433  leoprf  30499  leopsq  30500  cvnref  30662  gtiso  31042  fldextid  31743  prsss  31875  deranglem  33137  poxp2  33799  poxp3  33805  slerflex  33975  lrrecpo  34107  elfix2  34215  linedegen  34454  filnetlem2  34577  bj-ru0  35140  matunitlindflem2  35783  matunitlindf  35784  ftc1anclem3  35861  prdsbnd2  35962  reheibor  36006  ismgmOLD  36017  opidon2OLD  36021  exidreslem  36044  rngo2  36074  opideq  36485  eldmcoss2  36584  2xp3dxp2ge1d  40169  sn-inelr  40442  mzpf  40565  acongrep  40809  ttac  40865  mendval  41015  iocinico  41050  iocmbl  41051  seff  41934  sblpnf  41935  sigarid  44385  cnambpcma  44797  2leaddle2  44801  clintopval  45409  2arymaptfv  46008  2arymaptfo  46011  itcoval2  46021  itcoval3  46022