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  2164  eqeq12d  2776  rru  3737  dedth2v  4545  dedth3v  4546  dedth4v  4547  disjprsn  4675  opidg  4852  unisng  4885  intsng  4943  isso2i  5600  poinxp  5736  posn  5741  xpid11  5916  dfpo2  6294  predpoirr  6331  predfrirr  6332  f1oprswap  6863  f1o2sn  7138  residpr  7139  f1mpt  7258  f1eqcocnv  7302  isopolem  7346  3xpexg  7751  sqxpexg  7754  poxp  8126  poxp2  8141  poxp3  8148  oe0  8509  oecl  8524  nnmsucr  8613  ecopover  8821  enrefg  8990  php  9201  3xpfi  9290  dffi3  9401  elirrv  9569  infxpenlem  10016  isfin5  10301  isfin5-2  10393  pwfseqlem4a  10670  pwfseqlem4  10671  pwfseqlem5  10672  pwfseq  10673  nqereu  10938  halfnq  10985  ltsopr  11041  1idsr  11107  00sr  11108  sqgt0sr  11115  leid  11330  msqgt0  11758  msqge0  11759  recextlem1  11868  recextlem2  11869  recex  11870  div1  11928  cju  12238  2halves  12486  msqznn  12703  xrltnr  13170  xrleid  13202  iccid  13443  m1expeven  14173  sqneg  14179  sqcl  14182  nnsqcl  14192  qsqcl  14194  expubnd  14242  bernneq  14293  faclbnd  14354  faclbnd3  14356  hashfac  14523  leiso  14524  cjmulval  15232  fallrisefac  16112  sin2t  16265  cos2t  16266  divalglem0  16483  divalglem2  16485  gcd0id  16609  lcmid  16699  lcmgcdeq  16702  lcmfsn  16725  isprm5  16798  prslem  18385  pslem  18660  dirref  18689  efmndbasabf  18981  efmndhash  18985  efmndbasfi  18986  efmnd1bas  19002  submefmnd  19004  sgrp2nmndlem4  19040  grpsubid  19147  grp1inv  19171  cntzi  19456  symgbasfi  19506  symg1bas  19518  pgrpsubgsymg  19536  symgextfve  19546  pmtrfinv  19588  psgnsn  19647  ipeq0  21851  matsca2  22642  matbas2  22643  matplusgcell  22655  matsubgcell  22656  mamulid  22663  mamurid  22664  mattposcl  22675  mat1dimelbas  22693  mat1dimscm  22697  mat1dimmul  22698  m1detdiag  22819  mdetdiagid  22822  mdetunilem9  22842  matunitlindflem2  22902  matunitlindf  22903  pmatcoe1fsupp  22926  d1mat2pmat  22964  idcn  23482  hausdiag  23871  symgtgp  24332  ustref  24445  ustelimasn  24449  iducn  24508  ismet  24549  isxmet  24550  idnghm  24969  resubmet  25028  xrsxmet  25036  cphnm  25421  tcphnmval  25457  ipcau2  25462  tcphcphlem1  25463  tcphcphlem2  25464  tcphcph  25465  cmssmscld  25578  chordthmlem  27069  lesid  28003  lrrecpo  28206  subsid  28334  divs1  28469  zsoring  28674  ismot  28877  hmoval  31291  htth  31399  hvsubid  31507  hvnegid  31508  hv2times  31542  hiidrcl  31576  normval  31605  issh2  31690  chjidm  32001  normcan  32057  ho2times  32300  kbpj  32437  lnop0  32447  riesz3i  32543  leoprf  32609  leopsq  32610  cvnref  32772  gtiso  33173  fldextid  34169  prsss  34426  fineqvnttrclse  35650  deranglem  35745  elfix2  36481  linedegen  36723  filnetlem2  36998  ftc1anclem3  38444  prdsbnd2  38545  reheibor  38589  ismgmOLD  38600  opidon2OLD  38604  exidreslem  38627  rngo2  38657  opideq  39091  eldmcoss2  39297  mzpf  43581  acongrep  43821  ttac  43877  mendval  44020  iocinico  44053  iocmbl  44054  seff  45133  sblpnf  45134  sigarid  47686  cnambpcma  48182  2leaddle2  48186  grlicref  48928  clintopval  49119  2arymaptfv  49581  2arymaptfo  49584  itcoval2  49594  itcoval3  49595  resipos  49901  nelsubclem  49993  initoo2  50158  termoo2  50159  setc1onsubc  50528