Theorem anidms 566

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  sylancb  601  sylancbr  602  ru0  2133  eqeq12d  2753  rru  3726  dedth2v  4530  dedth3v  4531  dedth4v  4532  disjprsn  4659  opidg  4836  unisng  4869  intsng  4926  isso2i  5569  poinxp  5705  posn  5710  xpid11  5881  dfpo2  6254  predpoirr  6291  predfrirr  6292  f1oprswap  6819  f1o2sn  7089  residpr  7090  f1mpt  7209  f1eqcocnv  7249  isopolem  7293  3xpexg  7699  sqxpexg  7702  poxp  8071  poxp2  8086  poxp3  8093  oe0  8450  oecl  8465  nnmsucr  8554  ecopover  8761  enrefg  8924  php  9134  3xpfi  9224  dffi3  9337  infxpenlem  9926  isfin5  10212  isfin5-2  10304  pwfseqlem4a  10575  pwfseqlem4  10576  pwfseqlem5  10577  pwfseq  10578  nqereu  10843  halfnq  10890  ltsopr  10946  1idsr  11012  00sr  11013  sqgt0sr  11020  leid  11233  msqgt0  11661  msqge0  11662  recextlem1  11771  recextlem2  11772  recex  11773  div1  11835  cju  12146  2halves  12386  msqznn  12602  xrltnr  13061  xrleid  13093  iccid  13334  m1expeven  14062  sqneg  14068  sqcl  14071  nnsqcl  14081  qsqcl  14083  expubnd  14131  bernneq  14182  faclbnd  14243  faclbnd3  14245  hashfac  14411  leiso  14412  cjmulval  15098  fallrisefac  15981  sin2t  16135  cos2t  16136  divalglem0  16353  divalglem2  16355  gcd0id  16479  lcmid  16569  lcmgcdeq  16572  lcmfsn  16595  isprm5  16668  prslem  18254  pslem  18529  dirref  18558  efmndbasabf  18831  efmndhash  18835  efmndbasfi  18836  efmnd1bas  18852  submefmnd  18854  sgrp2nmndlem4  18890  grpsubid  18991  grp1inv  19015  cntzi  19295  symgbasfi  19345  symg1bas  19357  pgrpsubgsymg  19375  symgextfve  19385  pmtrfinv  19427  psgnsn  19486  ipeq0  21628  matsca2  22395  matbas2  22396  matplusgcell  22408  matsubgcell  22409  mamulid  22416  mamurid  22417  mattposcl  22428  mat1dimelbas  22446  mat1dimscm  22450  mat1dimmul  22451  m1detdiag  22572  mdetdiagid  22575  mdetunilem9  22595  pmatcoe1fsupp  22676  d1mat2pmat  22714  idcn  23232  hausdiag  23620  symgtgp  24081  ustref  24194  ustelimasn  24198  iducn  24257  ismet  24298  isxmet  24299  idnghm  24718  resubmet  24777  xrsxmet  24785  cphnm  25170  tcphnmval  25206  ipcau2  25211  tcphcphlem1  25212  tcphcphlem2  25213  tcphcph  25214  cmssmscld  25327  chordthmlem  26809  lesid  27745  lrrecpo  27947  subsid  28075  divs1  28210  zsoring  28415  ismot  28617  hmoval  30896  htth  31004  hvsubid  31112  hvnegid  31113  hv2times  31147  hiidrcl  31181  normval  31210  issh2  31295  chjidm  31606  normcan  31662  ho2times  31905  kbpj  32042  lnop0  32052  riesz3i  32148  leoprf  32214  leopsq  32215  cvnref  32377  gtiso  32789  fldextid  33819  prsss  34076  fineqvnttrclse  35284  deranglem  35364  elfix2  36100  linedegen  36341  filnetlem2  36577  matunitlindflem2  37952  matunitlindf  37953  ftc1anclem3  38030  prdsbnd2  38130  reheibor  38174  ismgmOLD  38185  opidon2OLD  38189  exidreslem  38212  rngo2  38242  opideq  38678  eldmcoss2  38884  mzpf  43182  acongrep  43426  ttac  43482  mendval  43625  iocinico  43658  iocmbl  43659  seff  44754  sblpnf  44755  sigarid  47304  cnambpcma  47754  2leaddle2  47758  grlicref  48500  clintopval  48692  2arymaptfv  49139  2arymaptfo  49142  itcoval2  49152  itcoval3  49153  resipos  49462  nelsubclem  49554  initoo2  49719  termoo2  49720  setc1onsubc  50089