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  2747  rru  3740  dedth2v  4553  dedth3v  4554  dedth4v  4555  disjprsn  4680  opidg  4854  unisng  4891  intsng  4951  isso2i  5585  poinxp  5717  posn  5722  xpid11  5892  dfpo2  6253  predpoirr  6292  predfrirr  6293  f1oprswap  6833  f1o2sn  7093  residpr  7094  f1mpt  7213  f1eqcocnv  7252  f1eqcocnvOLD  7253  isopolem  7295  3xpexg  7691  sqxpexg  7694  poxp  8065  poxp2  8080  poxp3  8087  oe0  8473  oecl  8488  nnmsucr  8577  ecopover  8767  enrefg  8931  php  9161  phpOLD  9173  3xpfi  9270  dffi3  9376  infxpenlem  9958  isfin5  10244  isfin5-2  10336  fpwwe2lem4  10579  pwfseqlem4a  10606  pwfseqlem4  10607  pwfseqlem5  10608  pwfseq  10609  nqereu  10874  halfnq  10921  ltsopr  10977  1idsr  11043  00sr  11044  sqgt0sr  11051  leid  11260  msqgt0  11684  msqge0  11685  recextlem1  11794  recextlem2  11795  recex  11796  div1  11853  cju  12158  2halves  12390  msqznn  12594  xrltnr  13049  xrleid  13080  iccid  13319  m1expeven  14025  sqneg  14031  sqcl  14033  nnsqcl  14043  qsqcl  14045  expubnd  14092  bernneq  14142  faclbnd  14200  faclbnd3  14202  hashfac  14369  leiso  14370  cjmulval  15042  fallrisefac  15919  sin2t  16070  cos2t  16071  divalglem0  16286  divalglem2  16288  gcd0id  16410  lcmid  16496  lcmgcdeq  16499  lcmfsn  16522  isprm5  16594  prslem  18201  pslem  18475  dirref  18504  efmndbasabf  18696  efmndhash  18700  efmndbasfi  18701  efmnd1bas  18717  submefmnd  18719  sgrp2nmndlem4  18752  grpsubid  18845  grp1inv  18869  cntzi  19123  permsetexOLD  19165  symgbasfi  19174  symg1bas  19186  pgrpsubgsymg  19205  symgextfve  19215  pmtrfinv  19257  psgnsn  19316  ipeq0  21079  matsca2  21806  matbas2  21807  matplusgcell  21819  matsubgcell  21820  mamulid  21827  mamurid  21828  mattposcl  21839  mat1dimelbas  21857  mat1dimscm  21861  mat1dimmul  21862  m1detdiag  21983  mdetdiagid  21986  mdetunilem9  22006  pmatcoe1fsupp  22087  d1mat2pmat  22125  idcn  22645  hausdiag  23033  symgtgp  23494  ustref  23607  ustelimasn  23611  iducn  23672  ismet  23713  isxmet  23714  idnghm  24144  resubmet  24202  xrsxmet  24209  cphnm  24594  tcphnmval  24630  ipcau2  24635  tcphcphlem1  24636  tcphcphlem2  24637  tcphcph  24638  cmssmscld  24751  chordthmlem  26219  slerflex  27148  lrrecpo  27296  subsid  27399  ismot  27540  hmoval  29815  htth  29923  hvsubid  30031  hvnegid  30032  hv2times  30066  hiidrcl  30100  normval  30129  issh2  30214  chjidm  30525  normcan  30581  ho2times  30824  kbpj  30961  lnop0  30971  riesz3i  31067  leoprf  31133  leopsq  31134  cvnref  31296  gtiso  31682  fldextid  32435  prsss  32586  deranglem  33847  elfix2  34565  linedegen  34804  filnetlem2  34927  bj-ru0  35486  matunitlindflem2  36148  matunitlindf  36149  ftc1anclem3  36226  prdsbnd2  36327  reheibor  36371  ismgmOLD  36382  opidon2OLD  36386  exidreslem  36409  rngo2  36439  opideq  36877  eldmcoss2  36994  2xp3dxp2ge1d  40687  sn-inelr  40992  mzpf  41117  acongrep  41362  ttac  41418  mendval  41568  iocinico  41604  iocmbl  41605  seff  42711  sblpnf  42712  sigarid  45219  cnambpcma  45646  2leaddle2  45650  clintopval  46258  2arymaptfv  46857  2arymaptfo  46860  itcoval2  46870  itcoval3  46871