Theorem anidms 571

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 208  df-an 397

This theorem is referenced by:  sylancb  606  sylancbr  607  ru0  2138  eqeq12d  2756  rru  3727  dedth2v  4524  dedth3v  4525  dedth4v  4526  disjprsn  4653  opidg  4830  unisng  4863  intsng  4920  isso2i  5570  poinxp  5706  posn  5711  xpid11  5881  dfpo2  6254  predpoirr  6291  predfrirr  6292  f1oprswap  6819  f1o2sn  7091  residpr  7092  f1mpt  7212  f1eqcocnv  7252  isopolem  7296  3xpexg  7702  sqxpexg  7705  poxp  8075  poxp2  8090  poxp3  8097  oe0  8454  oecl  8469  nnmsucr  8558  ecopover  8765  enrefg  8928  php  9138  3xpfi  9228  dffi3  9341  elirrv  9509  infxpenlem  9933  isfin5  10219  isfin5-2  10311  pwfseqlem4a  10582  pwfseqlem4  10583  pwfseqlem5  10584  pwfseq  10585  nqereu  10850  halfnq  10897  ltsopr  10953  1idsr  11019  00sr  11020  sqgt0sr  11027  leid  11240  msqgt0  11668  msqge0  11669  recextlem1  11778  recextlem2  11779  recex  11780  div1  11842  cju  12153  2halves  12393  msqznn  12609  xrltnr  13068  xrleid  13100  iccid  13341  m1expeven  14069  sqneg  14075  sqcl  14078  nnsqcl  14088  qsqcl  14090  expubnd  14138  bernneq  14189  faclbnd  14250  faclbnd3  14252  hashfac  14418  leiso  14419  cjmulval  15105  fallrisefac  15988  sin2t  16142  cos2t  16143  divalglem0  16360  divalglem2  16362  gcd0id  16486  lcmid  16576  lcmgcdeq  16579  lcmfsn  16602  isprm5  16675  prslem  18261  pslem  18536  dirref  18565  efmndbasabf  18838  efmndhash  18842  efmndbasfi  18843  efmnd1bas  18859  submefmnd  18861  sgrp2nmndlem4  18897  grpsubid  18998  grp1inv  19022  cntzi  19302  symgbasfi  19352  symg1bas  19364  pgrpsubgsymg  19382  symgextfve  19392  pmtrfinv  19434  psgnsn  19493  ipeq0  21620  matsca2  22410  matbas2  22411  matplusgcell  22423  matsubgcell  22424  mamulid  22431  mamurid  22432  mattposcl  22443  mat1dimelbas  22461  mat1dimscm  22465  mat1dimmul  22466  m1detdiag  22587  mdetdiagid  22590  mdetunilem9  22610  pmatcoe1fsupp  22691  d1mat2pmat  22729  idcn  23247  hausdiag  23635  symgtgp  24096  ustref  24209  ustelimasn  24213  iducn  24272  ismet  24313  isxmet  24314  idnghm  24733  resubmet  24792  xrsxmet  24800  cphnm  25185  tcphnmval  25221  ipcau2  25226  tcphcphlem1  25227  tcphcphlem2  25228  tcphcph  25229  cmssmscld  25342  chordthmlem  26821  lesid  27756  lrrecpo  27958  subsid  28086  divs1  28221  zsoring  28426  ismot  28628  hmoval  30906  htth  31014  hvsubid  31122  hvnegid  31123  hv2times  31157  hiidrcl  31191  normval  31220  issh2  31305  chjidm  31616  normcan  31672  ho2times  31915  kbpj  32052  lnop0  32062  riesz3i  32158  leoprf  32224  leopsq  32225  cvnref  32387  gtiso  32800  fldextid  33850  prsss  34107  fineqvnttrclse  35312  deranglem  35401  elfix2  36137  linedegen  36378  filnetlem2  36614  matunitlindflem2  37991  matunitlindf  37992  ftc1anclem3  38069  prdsbnd2  38169  reheibor  38213  ismgmOLD  38224  opidon2OLD  38228  exidreslem  38251  rngo2  38281  opideq  38717  eldmcoss2  38923  mzpf  43192  acongrep  43432  ttac  43488  mendval  43631  iocinico  43664  iocmbl  43665  seff  44760  sblpnf  44761  sigarid  47308  cnambpcma  47764  2leaddle2  47768  grlicref  48510  clintopval  48702  2arymaptfv  49149  2arymaptfo  49152  itcoval2  49162  itcoval3  49163  resipos  49472  nelsubclem  49564  initoo2  49729  termoo2  49730  setc1onsubc  50099