Theorem anidms 558

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

Syntax hints:   → wi 4   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  sylancb  589  sylancbr  590  dedth2v  4350  dedth3v  4351  dedth4v  4352  disjprsn  4452  opidg  4625  unisng  4656  intsng  4715  pwnss  5035  snex  5111  isso2i  5277  poinxp  5397  posn  5402  xpid11  5561  predpoirr  5934  predfrirr  5935  f1oprswap  6405  f1o2sn  6640  residpr  6641  f1mpt  6751  f1eqcocnv  6789  isopolem  6828  3xpexg  7200  sqxpexg  7202  poxp  7532  oe0  7848  oecl  7863  nnmsucr  7951  ecopover  8096  enrefg  8233  php  8392  3xpfi  8480  dffi3  8585  infxpenlem  9128  xp2cda  9296  isfin5-2  9507  fpwwe2lem5  9750  pwfseqlem4a  9777  pwfseqlem4  9778  pwfseqlem5  9779  pwfseq  9780  nqereu  10045  halfnq  10092  ltsopr  10148  1idsr  10213  00sr  10214  sqgt0sr  10221  leid  10427  msqgt0  10842  msqge0  10843  recextlem1  10951  recextlem2  10952  recex  10953  div1  11010  cju  11310  2halves  11546  msqznn  11744  xrltnr  12188  xrleid  12219  iccid  12457  m1expeven  13149  expubnd  13163  sqneg  13165  sqcl  13167  nnsqcl  13175  qsqcl  13177  subsq2  13215  bernneq  13232  faclbnd  13316  faclbnd3  13318  hashfac  13478  leiso  13479  cjmulval  14127  fallrisefac  14995  sin2t  15146  cos2t  15147  divalglem0  15355  divalglem2  15357  gcd0id  15478  lcmid  15560  lcmgcdeq  15563  lcmfsn  15586  isprm5  15655  prslem  17155  pslem  17430  dirref  17459  sgrp2nmndlem4  17639  grpsubid  17723  grp1inv  17747  cntzi  17982  symgval  18019  symgbas  18020  symgbasfi  18026  symg1bas  18036  pgrpsubgsymg  18048  symgextfve  18059  pmtrfinv  18101  psgnsn  18160  lsmidm  18297  ringadd2  18796  ipeq0  20212  matsca2  20456  matbas2  20457  matplusgcell  20469  matsubgcell  20470  mamulid  20477  mamurid  20478  mattposcl  20490  mat1dimelbas  20508  mat1dimscm  20512  mat1dimmul  20513  m1detdiag  20634  mdetdiagid  20637  mdetunilem9  20657  pmatcoe1fsupp  20739  d1mat2pmat  20777  idcn  21295  hausdiag  21682  symgtgp  22138  ustref  22255  ustelimasn  22259  iducn  22320  ismet  22361  isxmet  22362  idnghm  22780  resubmet  22838  xrsxmet  22845  cphnm  23225  tchnmval  23260  ipcau2  23265  tchcphlem1  23266  tchcphlem2  23267  tchcph  23268  chordthmlem  24795  ismot  25666  hmoval  28015  htth  28125  hvsubid  28233  hvnegid  28234  hv2times  28268  hiidrcl  28302  normval  28331  issh2  28416  chjidm  28729  normcan  28785  ho2times  29028  kbpj  29165  lnop0  29175  riesz3i  29271  leoprf  29337  leopsq  29338  cvnref  29500  gtiso  29827  prsss  30309  deranglem  31492  dfpo2  31988  elfix2  32353  linedegen  32592  filnetlem2  32716  bj-ru0  33261  matunitlindflem2  33737  matunitlindf  33738  ftc1anclem3  33817  prdsbnd2  33923  reheibor  33967  ismgmOLD  33978  opidon2OLD  33982  exidreslem  34005  rngo2  34035  opideq  34442  eldmcoss2  34540  mzpf  37818  acongrep  38065  ttac  38121  mendval  38271  mendplusgfval  38273  mendmulrfval  38275  iocinico  38314  iocmbl  38315  seff  39025  sblpnf  39026  sigarid  41546  cnambpcma  41902  2leaddle2  41905  clintopval  42425