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  2163  eqeq12d  2776  rru  3736  dedth2v  4544  dedth3v  4545  dedth4v  4546  disjprsn  4671  opidg  4851  unisng  4884  intsng  4942  isso2i  5595  poinxp  5731  posn  5736  xpid11  5913  dfpo2  6299  predpoirr  6336  predfrirr  6337  f1oprswap  6871  f1o2sn  7146  residpr  7147  f1mpt  7266  f1eqcocnv  7310  isopolem  7354  3xpexg  7767  sqxpexg  7770  poxp  8143  poxp2  8163  poxp3  8170  oe0  8534  oecl  8549  nnmsucr  8638  ecopover  8846  enrefg  9015  php  9226  3xpfi  9316  dffi3  9427  elirrv  9595  infxpenlem  10096  isfin5  10381  isfin5-2  10473  pwfseqlem4a  10750  pwfseqlem4  10751  pwfseqlem5  10752  pwfseq  10753  nqereu  11018  halfnq  11065  ltsopr  11121  1idsr  11187  00sr  11188  sqgt0sr  11195  leid  11410  msqgt0  11840  msqge0  11841  recextlem1  11950  recextlem2  11951  recex  11952  div1  12010  cju  12320  2halves  12568  msqznn  12785  xrltnr  13252  xrleid  13284  iccid  13525  m1expeven  14256  sqneg  14262  sqcl  14265  nnsqcl  14275  qsqcl  14277  expubnd  14325  bernneq  14377  faclbnd  14438  faclbnd3  14440  hashfac  14607  leiso  14608  cjmulval  15318  fallrisefac  16198  sin2t  16351  cos2t  16352  divalglem0  16569  divalglem2  16571  gcd0id  16697  lcmid  16790  lcmgcdeq  16793  lcmfsn  16816  isprm5  16889  prslem  18477  pslem  18752  dirref  18781  efmndbasabf  19074  efmndhash  19078  efmndbasfi  19079  efmnd1bas  19095  submefmnd  19097  sgrp2nmndlem4  19133  grpsubid  19240  grp1inv  19264  cntzi  19549  symgbasfi  19599  symg1bas  19611  pgrpsubgsymg  19629  symgextfve  19639  pmtrfinv  19681  psgnsn  19740  ipeq0  21950  matsca2  22741  matbas2  22742  matplusgcell  22754  matsubgcell  22755  mamulid  22762  mamurid  22763  mattposcl  22774  mat1dimelbas  22792  mat1dimscm  22796  mat1dimmul  22797  m1detdiag  22918  mdetdiagid  22921  mdetunilem9  22941  matunitlindflem2  23001  matunitlindf  23002  pmatcoe1fsupp  23025  d1mat2pmat  23063  idcn  23581  hausdiag  23970  symgtgp  24431  ustref  24544  ustelimasn  24548  iducn  24607  ismet  24648  isxmet  24649  idnghm  25068  resubmet  25127  xrsxmet  25135  cphnm  25520  tcphnmval  25556  ipcau2  25561  tcphcphlem1  25562  tcphcphlem2  25563  tcphcph  25564  cmssmscld  25677  chordthmlem  27166  lesid  28130  lrrecpo  28333  subsid  28461  divs1  28596  zsoring  28801  ismot  29004  hmoval  31418  htth  31526  hvsubid  31634  hvnegid  31635  hv2times  31669  hiidrcl  31703  normval  31732  issh2  31817  chjidm  32128  normcan  32184  ho2times  32427  kbpj  32564  lnop0  32574  riesz3i  32670  leoprf  32736  leopsq  32737  cvnref  32899  gtiso  33342  fldextid  34338  prsss  34595  fineqvnttrclse  35849  j0ltaleph  35948  deranglem  36018  elfix2  36759  linedegen  37001  filnetlem2  37260  ftc1anclem3  38707  prdsbnd2  38823  reheibor  38867  ismgmOLD  38878  opidon2OLD  38882  exidreslem  38905  rngo2  38935  opideq  39369  eldmcoss2  39575  mzpf  43841  acongrep  44081  ttac  44137  mendval  44275  iocinico  44308  iocmbl  44309  seff  45387  sblpnf  45388  omhf  46115  sigarid  47962  cnambpcma  48458  2leaddle2  48462  grlicref  49204  clintopval  49395  2arymaptfv  49857  2arymaptfo  49860  itcoval2  49870  itcoval3  49871  resipos  50183  nelsubclem  50275  initoo2  50448  termoo2  50449  setc1onsubc  50834  parhomidval  50840