Theorem anidms 675

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  sylancb  696  sylancbr  697  dedth2v  4093  dedth3v  4094  dedth4v  4095  disjprsn  4196  intsng  4447  pwnss  4756  snex  4835  isso2i  4991  poinxp  5105  posn  5110  xpid11  5268  predpoirr  5625  predfrirr  5626  f1oprswap  6092  f1o2sn  6314  residpr  6315  f1mpt  6419  f1eqcocnv  6456  isopolem  6495  3xpexg  6859  sqxpexg  6861  poxp  7176  oe0  7489  oecl  7504  nnmsucr  7592  ecopover  7738  ecopoverOLD  7739  enrefg  7873  php  8029  3xpfi  8117  dffi3  8220  infxpenlem  8719  xp2cda  8885  isfin5-2  9096  fpwwe2lem5  9335  pwfseqlem4a  9362  pwfseqlem4  9363  pwfseqlem5  9364  pwfseq  9365  nqereu  9630  halfnq  9677  ltsopr  9733  1idsr  9798  00sr  9799  sqgt0sr  9806  leid  10012  msqgt0  10427  msqge0  10428  recextlem1  10536  recextlem2  10537  recex  10538  div1  10595  cju  10893  2halves  11137  msqznn  11335  xrltnr  11829  xrleid  11859  iccid  12091  m1expeven  12769  expubnd  12783  sqneg  12785  sqcl  12787  nnsqcl  12795  qsqcl  12797  subsq2  12835  bernneq  12852  faclbnd  12939  faclbnd3  12941  hashfac  13099  leiso  13100  cjmulval  13733  fallrisefac  14595  sin2t  14746  cos2t  14747  divalglem0  14954  divalglem2  14956  gcd0id  15078  lcmid  15160  lcmgcdeq  15163  lcmfsn  15186  isprm5  15257  prslem  16754  pslem  17029  dirref  17058  sgrp2nmndlem4  17238  grpsubid  17322  grp1inv  17346  cntzi  17585  symgval  17622  symgbas  17623  symgbasfi  17629  symg1bas  17639  pgrpsubgsymg  17651  symgextfve  17662  pmtrfinv  17704  psgnsn  17763  lsmidm  17900  ringadd2  18398  ipeq0  19802  matsca2  20045  matbas2  20046  matplusgcell  20058  matsubgcell  20059  mamulid  20066  mamurid  20067  mattposcl  20078  mat1dimelbas  20096  mat1dimscm  20100  mat1dimmul  20101  m1detdiag  20222  mdetdiagid  20225  mdetunilem9  20245  pmatcoe1fsupp  20325  d1mat2pmat  20363  idcn  20871  hausdiag  21258  symgtgp  21715  ustref  21832  ustelimasn  21836  iducn  21897  ismet  21938  isxmet  21939  idnghm  22357  resubmet  22413  xrsxmet  22420  cphnm  22801  tchnmval  22836  ipcau2  22841  tchcphlem1  22842  tchcphlem2  22843  tchcph  22844  chordthmlem  24359  ismot  25230  is2wlkonot  26390  is2spthonot  26391  hmoval  27049  htth  27159  hvsubid  27267  hvnegid  27268  hv2times  27302  hiidrcl  27336  normval  27365  issh2  27450  chjidm  27763  normcan  27819  ho2times  28062  kbpj  28199  lnop0  28209  riesz3i  28305  leoprf  28371  leopsq  28372  cvnref  28534  gtiso  28861  prsss  29290  deranglem  30402  dfpo2  30898  elfix2  31181  linedegen  31420  filnetlem2  31544  bj-ru0  32124  matunitlindflem2  32576  matunitlindf  32577  ftc1anclem3  32657  prdsbnd2  32764  reheibor  32808  ismgmOLD  32819  opidon2OLD  32823  exidreslem  32846  rngo2  32876  mzpf  36317  acongrep  36565  ttac  36621  mendval  36772  mendplusgfval  36774  mendmulrfval  36776  iocinico  36816  iocmbl  36817  seff  37530  sblpnf  37531  sigarid  39696  opidg  40316  cnambpcma  40341  2leaddle2  40344  clintopval  41630