Theorem anidms 566

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

Syntax hints:   → wi 4   ∧ wa 395

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 396

This theorem is referenced by:  sylancb  599  sylancbr  600  eqeq12d  2754  rru  3709  dedth2v  4518  dedth3v  4519  dedth4v  4520  disjprsn  4647  opidg  4820  unisng  4857  intsng  4913  snex  5349  isso2i  5529  poinxp  5658  posn  5663  xpid11  5830  dfpo2  6188  predpoirr  6225  predfrirr  6226  f1oprswap  6743  f1o2sn  6996  residpr  6997  f1mpt  7115  f1eqcocnv  7153  f1eqcocnvOLD  7154  isopolem  7196  3xpexg  7580  sqxpexg  7583  poxp  7940  oe0  8314  oecl  8329  nnmsucr  8418  ecopover  8568  enrefg  8727  php  8897  3xpfi  9016  dffi3  9120  infxpenlem  9700  isfin5  9986  isfin5-2  10078  fpwwe2lem4  10321  pwfseqlem4a  10348  pwfseqlem4  10349  pwfseqlem5  10350  pwfseq  10351  nqereu  10616  halfnq  10663  ltsopr  10719  1idsr  10785  00sr  10786  sqgt0sr  10793  leid  11001  msqgt0  11425  msqge0  11426  recextlem1  11535  recextlem2  11536  recex  11537  div1  11594  cju  11899  2halves  12131  msqznn  12332  xrltnr  12784  xrleid  12814  iccid  13053  m1expeven  13758  sqneg  13764  sqcl  13766  nnsqcl  13775  qsqcl  13777  expubnd  13823  bernneq  13872  faclbnd  13932  faclbnd3  13934  hashfac  14100  leiso  14101  cjmulval  14784  fallrisefac  15663  sin2t  15814  cos2t  15815  divalglem0  16030  divalglem2  16032  gcd0id  16154  lcmid  16242  lcmgcdeq  16245  lcmfsn  16268  isprm5  16340  prslem  17931  pslem  18205  dirref  18234  efmndbasabf  18426  efmndhash  18430  efmndbasfi  18431  efmnd1bas  18447  submefmnd  18449  sgrp2nmndlem4  18482  grpsubid  18574  grp1inv  18598  cntzi  18850  permsetexOLD  18892  symgbasfi  18901  symg1bas  18913  pgrpsubgsymg  18932  symgextfve  18942  pmtrfinv  18984  psgnsn  19043  lsmidmOLD  19184  ringadd2  19729  ipeq0  20755  matsca2  21477  matbas2  21478  matplusgcell  21490  matsubgcell  21491  mamulid  21498  mamurid  21499  mattposcl  21510  mat1dimelbas  21528  mat1dimscm  21532  mat1dimmul  21533  m1detdiag  21654  mdetdiagid  21657  mdetunilem9  21677  pmatcoe1fsupp  21758  d1mat2pmat  21796  idcn  22316  hausdiag  22704  symgtgp  23165  ustref  23278  ustelimasn  23282  iducn  23343  ismet  23384  isxmet  23385  idnghm  23813  resubmet  23871  xrsxmet  23878  cphnm  24262  tcphnmval  24298  ipcau2  24303  tcphcphlem1  24304  tcphcphlem2  24305  tcphcph  24306  cmssmscld  24419  chordthmlem  25887  ismot  26800  hmoval  29073  htth  29181  hvsubid  29289  hvnegid  29290  hv2times  29324  hiidrcl  29358  normval  29387  issh2  29472  chjidm  29783  normcan  29839  ho2times  30082  kbpj  30219  lnop0  30229  riesz3i  30325  leoprf  30391  leopsq  30392  cvnref  30554  gtiso  30935  fldextid  31636  prsss  31768  deranglem  33028  poxp2  33717  poxp3  33723  slerflex  33893  lrrecpo  34025  elfix2  34133  linedegen  34372  filnetlem2  34495  bj-ru0  35058  matunitlindflem2  35701  matunitlindf  35702  ftc1anclem3  35779  prdsbnd2  35880  reheibor  35924  ismgmOLD  35935  opidon2OLD  35939  exidreslem  35962  rngo2  35992  opideq  36405  eldmcoss2  36504  2xp3dxp2ge1d  40090  sn-inelr  40356  mzpf  40474  acongrep  40718  ttac  40774  mendval  40924  iocinico  40959  iocmbl  40960  seff  41816  sblpnf  41817  sigarid  44261  cnambpcma  44674  2leaddle2  44678  clintopval  45286  2arymaptfv  45885  2arymaptfo  45888  itcoval2  45898  itcoval3  45899