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

This theorem is referenced by:  sylancb  599  sylancbr  600  rru  3704  dedth2v  4441  dedth3v  4442  dedth4v  4443  disjprsn  4557  opidg  4729  unisng  4760  intsng  4817  snex  5223  isso2i  5396  poinxp  5518  posn  5523  xpid11  5684  predpoirr  6051  predfrirr  6052  f1oprswap  6526  f1o2sn  6767  residpr  6768  f1mpt  6884  f1eqcocnv  6922  isopolem  6961  3xpexg  7332  sqxpexg  7334  poxp  7675  oe0  7998  oecl  8013  nnmsucr  8101  ecopover  8251  enrefg  8389  php  8548  3xpfi  8636  dffi3  8741  infxpenlem  9285  isfin5  9567  isfin5-2  9659  fpwwe2lem5  9902  pwfseqlem4a  9929  pwfseqlem4  9930  pwfseqlem5  9931  pwfseq  9932  nqereu  10197  halfnq  10244  ltsopr  10300  1idsr  10366  00sr  10367  sqgt0sr  10374  leid  10583  msqgt0  11008  msqge0  11009  recextlem1  11118  recextlem2  11119  recex  11120  div1  11177  cju  11482  2halves  11713  msqznn  11913  xrltnr  12364  xrleid  12394  iccid  12633  m1expeven  13326  sqneg  13332  sqcl  13334  nnsqcl  13343  qsqcl  13345  expubnd  13391  bernneq  13440  faclbnd  13500  faclbnd3  13502  hashfac  13664  leiso  13665  cjmulval  14338  fallrisefac  15212  sin2t  15363  cos2t  15364  divalglem0  15577  divalglem2  15579  gcd0id  15700  lcmid  15782  lcmgcdeq  15785  lcmfsn  15808  isprm5  15880  prslem  17370  pslem  17645  dirref  17674  sgrp2nmndlem4  17854  grpsubid  17940  grp1inv  17964  cntzi  18200  symgval  18238  symgbas  18239  symgbasfi  18245  symg1bas  18255  pgrpsubgsymg  18267  symgextfve  18278  pmtrfinv  18320  psgnsn  18379  lsmidm  18517  ringadd2  19015  ipeq0  20464  matsca2  20713  matbas2  20714  matplusgcell  20726  matsubgcell  20727  mamulid  20734  mamurid  20735  mattposcl  20746  mat1dimelbas  20764  mat1dimscm  20768  mat1dimmul  20769  m1detdiag  20890  mdetdiagid  20893  mdetunilem9  20913  pmatcoe1fsupp  20993  d1mat2pmat  21031  idcn  21549  hausdiag  21937  symgtgp  22393  ustref  22510  ustelimasn  22514  iducn  22575  ismet  22616  isxmet  22617  idnghm  23035  resubmet  23093  xrsxmet  23100  cphnm  23480  tcphnmval  23515  ipcau2  23520  tcphcphlem1  23521  tcphcphlem2  23522  tcphcph  23523  cmssmscld  23636  chordthmlem  25091  ismot  26003  hmoval  28278  htth  28386  hvsubid  28494  hvnegid  28495  hv2times  28529  hiidrcl  28563  normval  28592  issh2  28677  chjidm  28988  normcan  29044  ho2times  29287  kbpj  29424  lnop0  29434  riesz3i  29530  leoprf  29596  leopsq  29597  cvnref  29759  gtiso  30124  fldextid  30653  prsss  30776  deranglem  32021  dfpo2  32599  elfix2  32974  linedegen  33213  filnetlem2  33336  bj-ru0  33824  matunitlindflem2  34420  matunitlindf  34421  ftc1anclem3  34500  prdsbnd2  34605  reheibor  34649  ismgmOLD  34660  opidon2OLD  34664  exidreslem  34687  rngo2  34717  opideq  35132  eldmcoss2  35230  mzpf  38818  acongrep  39062  ttac  39118  mendval  39268  mendplusgfval  39270  mendmulrfval  39272  iocinico  39303  iocmbl  39304  seff  40179  sblpnf  40180  sigarid  42657  cnambpcma  43010  2leaddle2  43014  clintopval  43589