Theorem anidms 574

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  sylancb  609  sylancbr  610  ru0  2160  eqeq12d  2777  rru  3740  dedth2v  4540  dedth3v  4541  dedth4v  4542  disjprsn  4670  opidg  4847  unisng  4880  intsng  4938  isso2i  5588  poinxp  5724  posn  5729  xpid11  5904  dfpo2  6277  predpoirr  6314  predfrirr  6315  f1oprswap  6846  f1o2sn  7118  residpr  7119  f1mpt  7239  f1eqcocnv  7279  isopolem  7323  3xpexg  7729  sqxpexg  7732  poxp  8101  poxp2  8116  poxp3  8123  oe0  8484  oecl  8499  nnmsucr  8588  ecopover  8796  enrefg  8958  php  9168  3xpfi  9258  dffi3  9370  elirrv  9538  infxpenlem  9962  isfin5  10249  isfin5-2  10341  pwfseqlem4a  10612  pwfseqlem4  10613  pwfseqlem5  10614  pwfseq  10615  nqereu  10880  halfnq  10927  ltsopr  10983  1idsr  11049  00sr  11050  sqgt0sr  11057  leid  11272  msqgt0  11700  msqge0  11701  recextlem1  11810  recextlem2  11811  recex  11812  div1  11873  cju  12184  2halves  12432  msqznn  12648  xrltnr  13114  xrleid  13146  iccid  13387  m1expeven  14115  sqneg  14121  sqcl  14124  nnsqcl  14134  qsqcl  14136  expubnd  14184  bernneq  14235  faclbnd  14296  faclbnd3  14298  hashfac  14464  leiso  14465  cjmulval  15162  fallrisefac  16045  sin2t  16199  cos2t  16200  divalglem0  16417  divalglem2  16419  gcd0id  16543  lcmid  16633  lcmgcdeq  16636  lcmfsn  16659  isprm5  16732  prslem  18319  pslem  18594  dirref  18623  efmndbasabf  18896  efmndhash  18900  efmndbasfi  18901  efmnd1bas  18917  submefmnd  18919  sgrp2nmndlem4  18955  grpsubid  19056  grp1inv  19080  cntzi  19359  symgbasfi  19409  symg1bas  19421  pgrpsubgsymg  19439  symgextfve  19449  pmtrfinv  19491  psgnsn  19550  ipeq0  21677  matsca2  22467  matbas2  22468  matplusgcell  22480  matsubgcell  22481  mamulid  22488  mamurid  22489  mattposcl  22500  mat1dimelbas  22518  mat1dimscm  22522  mat1dimmul  22523  m1detdiag  22644  mdetdiagid  22647  mdetunilem9  22667  pmatcoe1fsupp  22748  d1mat2pmat  22786  idcn  23304  hausdiag  23692  symgtgp  24153  ustref  24266  ustelimasn  24270  iducn  24329  ismet  24370  isxmet  24371  idnghm  24790  resubmet  24849  xrsxmet  24857  cphnm  25242  tcphnmval  25278  ipcau2  25283  tcphcphlem1  25284  tcphcphlem2  25285  tcphcph  25286  cmssmscld  25399  chordthmlem  26884  lesid  27818  lrrecpo  28021  subsid  28149  divs1  28284  zsoring  28489  ismot  28691  hmoval  30969  htth  31077  hvsubid  31185  hvnegid  31186  hv2times  31220  hiidrcl  31254  normval  31283  issh2  31368  chjidm  31679  normcan  31735  ho2times  31978  kbpj  32115  lnop0  32125  riesz3i  32221  leoprf  32287  leopsq  32288  cvnref  32450  gtiso  32863  fldextid  33916  prsss  34173  fineqvnttrclse  35380  deranglem  35476  elfix2  36212  linedegen  36453  filnetlem2  36699  matunitlindflem2  38076  matunitlindf  38077  ftc1anclem3  38154  prdsbnd2  38254  reheibor  38298  ismgmOLD  38309  opidon2OLD  38313  exidreslem  38336  rngo2  38366  opideq  38802  eldmcoss2  39008  mzpf  43277  acongrep  43517  ttac  43573  mendval  43716  iocinico  43749  iocmbl  43750  seff  44845  sblpnf  44846  sigarid  47392  cnambpcma  47848  2leaddle2  47852  grlicref  48594  clintopval  48786  2arymaptfv  49233  2arymaptfo  49236  itcoval2  49246  itcoval3  49247  resipos  49556  nelsubclem  49648  initoo2  49813  termoo2  49814  setc1onsubc  50183