Theorem anidms 570

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  sylancb  603  sylancbr  604  eqeq12d  2753  rru  3692  dedth2v  4501  dedth3v  4502  dedth4v  4503  disjprsn  4630  opidg  4803  unisng  4840  intsng  4896  snex  5324  isso2i  5503  poinxp  5629  posn  5634  xpid11  5801  predpoirr  6191  predfrirr  6192  f1oprswap  6704  f1o2sn  6957  residpr  6958  f1mpt  7073  f1eqcocnv  7111  f1eqcocnvOLD  7112  isopolem  7154  3xpexg  7537  sqxpexg  7540  poxp  7895  oe0  8249  oecl  8264  nnmsucr  8353  ecopover  8503  enrefg  8660  php  8830  3xpfi  8943  dffi3  9047  infxpenlem  9627  isfin5  9913  isfin5-2  10005  fpwwe2lem4  10248  pwfseqlem4a  10275  pwfseqlem4  10276  pwfseqlem5  10277  pwfseq  10278  nqereu  10543  halfnq  10590  ltsopr  10646  1idsr  10712  00sr  10713  sqgt0sr  10720  leid  10928  msqgt0  11352  msqge0  11353  recextlem1  11462  recextlem2  11463  recex  11464  div1  11521  cju  11826  2halves  12058  msqznn  12259  xrltnr  12711  xrleid  12741  iccid  12980  m1expeven  13682  sqneg  13688  sqcl  13690  nnsqcl  13699  qsqcl  13701  expubnd  13747  bernneq  13796  faclbnd  13856  faclbnd3  13858  hashfac  14024  leiso  14025  cjmulval  14708  fallrisefac  15587  sin2t  15738  cos2t  15739  divalglem0  15954  divalglem2  15956  gcd0id  16078  lcmid  16166  lcmgcdeq  16169  lcmfsn  16192  isprm5  16264  prslem  17805  pslem  18078  dirref  18107  efmndbasabf  18299  efmndhash  18303  efmndbasfi  18304  efmnd1bas  18320  submefmnd  18322  sgrp2nmndlem4  18355  grpsubid  18447  grp1inv  18471  cntzi  18723  permsetexOLD  18762  symgbasfi  18771  symg1bas  18783  pgrpsubgsymg  18801  symgextfve  18811  pmtrfinv  18853  psgnsn  18912  lsmidmOLD  19053  ringadd2  19593  ipeq0  20600  matsca2  21317  matbas2  21318  matplusgcell  21330  matsubgcell  21331  mamulid  21338  mamurid  21339  mattposcl  21350  mat1dimelbas  21368  mat1dimscm  21372  mat1dimmul  21373  m1detdiag  21494  mdetdiagid  21497  mdetunilem9  21517  pmatcoe1fsupp  21598  d1mat2pmat  21636  idcn  22154  hausdiag  22542  symgtgp  23003  ustref  23116  ustelimasn  23120  iducn  23180  ismet  23221  isxmet  23222  idnghm  23641  resubmet  23699  xrsxmet  23706  cphnm  24090  tcphnmval  24126  ipcau2  24131  tcphcphlem1  24132  tcphcphlem2  24133  tcphcph  24134  cmssmscld  24247  chordthmlem  25715  ismot  26626  hmoval  28891  htth  28999  hvsubid  29107  hvnegid  29108  hv2times  29142  hiidrcl  29176  normval  29205  issh2  29290  chjidm  29601  normcan  29657  ho2times  29900  kbpj  30037  lnop0  30047  riesz3i  30143  leoprf  30209  leopsq  30210  cvnref  30372  gtiso  30753  fldextid  31448  prsss  31580  deranglem  32841  dfpo2  33441  poxp2  33527  poxp3  33533  slerflex  33703  lrrecpo  33835  elfix2  33943  linedegen  34182  filnetlem2  34305  bj-ru0  34868  matunitlindflem2  35511  matunitlindf  35512  ftc1anclem3  35589  prdsbnd2  35690  reheibor  35734  ismgmOLD  35745  opidon2OLD  35749  exidreslem  35772  rngo2  35802  opideq  36215  eldmcoss2  36314  2xp3dxp2ge1d  39884  sn-inelr  40143  mzpf  40261  acongrep  40505  ttac  40561  mendval  40711  iocinico  40746  iocmbl  40747  seff  41600  sblpnf  41601  sigarid  44046  cnambpcma  44459  2leaddle2  44463  clintopval  45071  2arymaptfv  45670  2arymaptfo  45673  itcoval2  45683  itcoval3  45684