Theorem anidms 577

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sylancb  612  sylancbr  613  ru0  2165  eqeq12d  2781  rru  3744  dedth2v  4552  dedth3v  4553  dedth4v  4554  disjprsn  4682  opidg  4859  unisng  4892  intsng  4950  isso2i  5608  poinxp  5744  posn  5749  xpid11  5924  dfpo2  6301  predpoirr  6338  predfrirr  6339  f1oprswap  6870  f1o2sn  7142  residpr  7143  f1mpt  7261  f1eqcocnv  7305  isopolem  7349  3xpexg  7753  sqxpexg  7756  poxp  8126  poxp2  8141  poxp3  8148  oe0  8509  oecl  8524  nnmsucr  8613  ecopover  8821  enrefg  8983  php  9194  3xpfi  9283  dffi3  9394  elirrv  9562  infxpenlem  10009  isfin5  10294  isfin5-2  10386  pwfseqlem4a  10657  pwfseqlem4  10658  pwfseqlem5  10659  pwfseq  10660  nqereu  10925  halfnq  10972  ltsopr  11028  1idsr  11094  00sr  11095  sqgt0sr  11102  leid  11317  msqgt0  11745  msqge0  11746  recextlem1  11855  recextlem2  11856  recex  11857  div1  11915  cju  12225  2halves  12473  msqznn  12689  xrltnr  13155  xrleid  13187  iccid  13428  m1expeven  14158  sqneg  14164  sqcl  14167  nnsqcl  14177  qsqcl  14179  expubnd  14227  bernneq  14278  faclbnd  14339  faclbnd3  14341  hashfac  14508  leiso  14509  cjmulval  15215  fallrisefac  16097  sin2t  16250  cos2t  16251  divalglem0  16468  divalglem2  16470  gcd0id  16594  lcmid  16684  lcmgcdeq  16687  lcmfsn  16710  isprm5  16783  prslem  18370  pslem  18645  dirref  18674  efmndbasabf  18954  efmndhash  18958  efmndbasfi  18959  efmnd1bas  18975  submefmnd  18977  sgrp2nmndlem4  19013  grpsubid  19113  grp1inv  19137  cntzi  19422  symgbasfi  19472  symg1bas  19484  pgrpsubgsymg  19502  symgextfve  19512  pmtrfinv  19554  psgnsn  19613  ipeq0  21817  matsca2  22606  matbas2  22607  matplusgcell  22619  matsubgcell  22620  mamulid  22627  mamurid  22628  mattposcl  22639  mat1dimelbas  22657  mat1dimscm  22661  mat1dimmul  22662  m1detdiag  22783  mdetdiagid  22786  mdetunilem9  22806  pmatcoe1fsupp  22887  d1mat2pmat  22925  idcn  23443  hausdiag  23831  symgtgp  24292  ustref  24405  ustelimasn  24409  iducn  24468  ismet  24509  isxmet  24510  idnghm  24929  resubmet  24988  xrsxmet  24996  cphnm  25381  tcphnmval  25417  ipcau2  25422  tcphcphlem1  25423  tcphcphlem2  25424  tcphcph  25425  cmssmscld  25538  chordthmlem  27026  lesid  27960  lrrecpo  28163  subsid  28291  divs1  28426  zsoring  28631  ismot  28833  hmoval  31191  htth  31299  hvsubid  31407  hvnegid  31408  hv2times  31442  hiidrcl  31476  normval  31505  issh2  31590  chjidm  31901  normcan  31957  ho2times  32200  kbpj  32337  lnop0  32347  riesz3i  32443  leoprf  32509  leopsq  32510  cvnref  32672  gtiso  33075  fldextid  34072  prsss  34329  fineqvnttrclse  35553  deranglem  35671  elfix2  36407  linedegen  36648  filnetlem2  36923  matunitlindflem2  38301  matunitlindf  38302  ftc1anclem3  38379  prdsbnd2  38479  reheibor  38523  ismgmOLD  38534  opidon2OLD  38538  exidreslem  38561  rngo2  38591  opideq  39025  eldmcoss2  39231  mzpf  43500  acongrep  43740  ttac  43796  mendval  43939  iocinico  43972  iocmbl  43973  seff  45052  sblpnf  45053  sigarid  47605  cnambpcma  48064  2leaddle2  48068  grlicref  48810  clintopval  49002  2arymaptfv  49464  2arymaptfo  49467  itcoval2  49477  itcoval3  49478  resipos  49786  nelsubclem  49878  initoo2  50043  termoo2  50044  setc1onsubc  50413