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  2166  eqeq12d  2779  rur  3740  dedth2v  4548  dedth3v  4549  dedth4v  4550  disjprsn  4676  opidg  4857  unisng  4890  intsng  4948  isso2i  5603  poinxp  5740  posn  5745  xpid11  5926  dfpo2  6325  predpoirr  6362  predfrirr  6363  f1oprswap  6901  f1o2sn  7177  residpr  7178  f1mpt  7296  f1eqcocnv  7340  isopolem  7384  3xpexg  7798  sqxpexg  7801  poxp  8177  poxp2  8197  poxp3  8204  oe0  8568  oecl  8583  nnmsucr  8672  ecopover  8880  enrefg  9049  php  9260  3xpfi  9350  dffi3  9460  elirrv  9628  infxpenlem  10131  isfin5  10416  isfin5-2  10508  pwfseqlem4a  10785  pwfseqlem4  10786  pwfseqlem5  10787  pwfseq  10788  nqereu  11053  halfnq  11100  ltsopr  11156  1idsr  11222  00sr  11223  sqgt0sr  11230  leid  11445  msqgt0  11876  msqge0  11877  recextlem1  11986  recextlem2  11987  recex  11988  div1  12046  cju  12356  2halves  12604  msqznn  12821  xrltnr  13288  xrleid  13320  iccid  13561  m1expeven  14292  sqneg  14298  sqcl  14301  nnsqcl  14311  qsqcl  14313  expubnd  14361  bernneq  14414  faclbnd  14475  faclbnd3  14477  hashfac  14644  leiso  14645  cjmulval  15355  fallrisefac  16236  sin2t  16389  cos2t  16390  divalglem0  16607  divalglem2  16609  gcd0id  16735  lcmid  16828  lcmgcdeq  16831  lcmfsn  16854  isprm5  16927  prslem  18521  pslem  18796  dirref  18825  efmndbasabf  19118  efmndhash  19122  efmndbasfi  19123  efmnd1bas  19139  submefmnd  19141  sgrp2nmndlem4  19177  grpsubid  19284  grp1inv  19308  cntzi  19594  symgbasfi  19644  symg1bas  19656  pgrpsubgsymg  19674  symgextfve  19684  pmtrfinv  19726  psgnsn  19785  ipeq0  21999  matsca2  22790  matbas2  22791  matplusgcell  22803  matsubgcell  22804  mamulid  22811  mamurid  22812  mattposcl  22823  mat1dimelbas  22841  mat1dimscm  22845  mat1dimmul  22846  m1detdiag  22967  mdetdiagid  22970  mdetunilem9  22990  matunitlindflem2  23050  matunitlindf  23051  pmatcoe1fsupp  23074  d1mat2pmat  23112  idcn  23630  hausdiag  24019  symgtgp  24480  ustref  24593  ustelimasn  24597  iducn  24656  ismet  24697  isxmet  24698  idnghm  25117  resubmet  25176  xrsxmet  25184  cphnm  25569  tcphnmval  25605  ipcau2  25610  tcphcphlem1  25611  tcphcphlem2  25612  tcphcph  25613  cmssmscld  25726  chordthmlem  27217  lesid  28181  lrrecpo  28384  subsid  28512  divs1  28647  zsoring  28852  ismot  29055  hmoval  31469  htth  31577  hvsubid  31685  hvnegid  31686  hv2times  31720  hiidrcl  31754  normval  31783  issh2  31868  chjidm  32179  normcan  32235  ho2times  32478  kbpj  32615  lnop0  32625  riesz3i  32721  leoprf  32787  leopsq  32788  cvnref  32950  gtiso  33391  fldextid  34402  prsss  34659  fineqvnttrclse  35933  j0ltaleph  36049  deranglem  36139  elfix2  36881  linedegen  37123  filnetlem2  37382  ftc1anclem3  38881  prdsbnd2  38995  reheibor  39039  ismgmOLD  39050  opidon2OLD  39054  exidreslem  39077  rngo2  39107  opideq  39541  eldmcoss2  39747  mzpf  44013  acongrep  44253  ttac  44309  mendval  44442  iocinico  44475  iocmbl  44476  seff  45554  sblpnf  45555  omhf  46285  sigarid  48141  cnambpcma  48637  2leaddle2  48641  grlicref  49383  clintopval  49574  2arymaptfv  50094  2arymaptfo  50097  itcoval2  50107  itcoval3  50108  resipos  50420  nelsubclem  50512  initoo2  50685  termoo2  50686  setc1onsubc  51071  parhomidval  51077  coshsinhsq  51260