Theorem anidms 677

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  sylancb  699  sylancbr  700  dedth2v  4143  dedth3v  4144  dedth4v  4145  disjprsn  4250  intsng  4512  pwnss  4830  snex  4908  isso2i  5067  poinxp  5182  posn  5187  xpid11  5347  predpoirr  5708  predfrirr  5709  f1oprswap  6180  f1o2sn  6408  residpr  6409  f1mpt  6518  f1eqcocnv  6556  isopolem  6595  3xpexg  6961  sqxpexg  6963  poxp  7289  oe0  7602  oecl  7617  nnmsucr  7705  ecopover  7851  ecopoverOLD  7852  enrefg  7987  php  8144  3xpfi  8232  dffi3  8337  infxpenlem  8836  xp2cda  9002  isfin5-2  9213  fpwwe2lem5  9456  pwfseqlem4a  9483  pwfseqlem4  9484  pwfseqlem5  9485  pwfseq  9486  nqereu  9751  halfnq  9798  ltsopr  9854  1idsr  9919  00sr  9920  sqgt0sr  9927  leid  10133  msqgt0  10548  msqge0  10549  recextlem1  10657  recextlem2  10658  recex  10659  div1  10716  cju  11016  2halves  11260  msqznn  11459  xrltnr  11953  xrleid  11983  iccid  12220  m1expeven  12907  expubnd  12921  sqneg  12923  sqcl  12925  nnsqcl  12933  qsqcl  12935  subsq2  12973  bernneq  12990  faclbnd  13077  faclbnd3  13079  hashfac  13242  leiso  13243  cjmulval  13885  fallrisefac  14756  sin2t  14907  cos2t  14908  divalglem0  15116  divalglem2  15118  gcd0id  15240  lcmid  15322  lcmgcdeq  15325  lcmfsn  15348  isprm5  15419  prslem  16931  pslem  17206  dirref  17235  sgrp2nmndlem4  17415  grpsubid  17499  grp1inv  17523  cntzi  17762  symgval  17799  symgbas  17800  symgbasfi  17806  symg1bas  17816  pgrpsubgsymg  17828  symgextfve  17839  pmtrfinv  17881  psgnsn  17940  lsmidm  18077  ringadd2  18575  ipeq0  19983  matsca2  20226  matbas2  20227  matplusgcell  20239  matsubgcell  20240  mamulid  20247  mamurid  20248  mattposcl  20259  mat1dimelbas  20277  mat1dimscm  20281  mat1dimmul  20282  m1detdiag  20403  mdetdiagid  20406  mdetunilem9  20426  pmatcoe1fsupp  20506  d1mat2pmat  20544  idcn  21061  hausdiag  21448  symgtgp  21905  ustref  22022  ustelimasn  22026  iducn  22087  ismet  22128  isxmet  22129  idnghm  22547  resubmet  22605  xrsxmet  22612  cphnm  22993  tchnmval  23028  ipcau2  23033  tchcphlem1  23034  tchcphlem2  23035  tchcph  23036  chordthmlem  24559  ismot  25430  hmoval  27665  htth  27775  hvsubid  27883  hvnegid  27884  hv2times  27918  hiidrcl  27952  normval  27981  issh2  28066  chjidm  28379  normcan  28435  ho2times  28678  kbpj  28815  lnop0  28825  riesz3i  28921  leoprf  28987  leopsq  28988  cvnref  29150  gtiso  29478  prsss  29962  deranglem  31148  dfpo2  31645  elfix2  32011  linedegen  32250  filnetlem2  32374  bj-ru0  32932  matunitlindflem2  33406  matunitlindf  33407  ftc1anclem3  33487  prdsbnd2  33594  reheibor  33638  ismgmOLD  33649  opidon2OLD  33653  exidreslem  33676  rngo2  33706  opidORIG  34109  mzpf  37299  acongrep  37547  ttac  37603  mendval  37753  mendplusgfval  37755  mendmulrfval  37757  iocinico  37797  iocmbl  37798  seff  38508  sblpnf  38509  sigarid  41047  opidg  41297  cnambpcma  41309  2leaddle2  41312  clintopval  41840