Theorem anidms 568

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  sylancb  601  sylancbr  602  eqeq12d  2749  rru  3776  dedth2v  4591  dedth3v  4592  dedth4v  4593  disjprsn  4719  opidg  4893  unisng  4930  intsng  4990  isso2i  5624  poinxp  5757  posn  5762  xpid11  5932  dfpo2  6296  predpoirr  6335  predfrirr  6336  f1oprswap  6878  f1o2sn  7140  residpr  7141  f1mpt  7260  f1eqcocnv  7299  f1eqcocnvOLD  7300  isopolem  7342  3xpexg  7739  sqxpexg  7742  poxp  8114  poxp2  8129  poxp3  8136  oe0  8522  oecl  8537  nnmsucr  8625  ecopover  8815  enrefg  8980  php  9210  phpOLD  9222  3xpfi  9319  dffi3  9426  infxpenlem  10008  isfin5  10294  isfin5-2  10386  fpwwe2lem4  10629  pwfseqlem4a  10656  pwfseqlem4  10657  pwfseqlem5  10658  pwfseq  10659  nqereu  10924  halfnq  10971  ltsopr  11027  1idsr  11093  00sr  11094  sqgt0sr  11101  leid  11310  msqgt0  11734  msqge0  11735  recextlem1  11844  recextlem2  11845  recex  11846  div1  11903  cju  12208  2halves  12440  msqznn  12644  xrltnr  13099  xrleid  13130  iccid  13369  m1expeven  14075  sqneg  14081  sqcl  14083  nnsqcl  14093  qsqcl  14095  expubnd  14142  bernneq  14192  faclbnd  14250  faclbnd3  14252  hashfac  14419  leiso  14420  cjmulval  15092  fallrisefac  15969  sin2t  16120  cos2t  16121  divalglem0  16336  divalglem2  16338  gcd0id  16460  lcmid  16546  lcmgcdeq  16549  lcmfsn  16572  isprm5  16644  prslem  18251  pslem  18525  dirref  18554  efmndbasabf  18753  efmndhash  18757  efmndbasfi  18758  efmnd1bas  18774  submefmnd  18776  sgrp2nmndlem4  18809  grpsubid  18907  grp1inv  18931  cntzi  19193  permsetexOLD  19237  symgbasfi  19246  symg1bas  19258  pgrpsubgsymg  19277  symgextfve  19287  pmtrfinv  19329  psgnsn  19388  ipeq0  21191  matsca2  21922  matbas2  21923  matplusgcell  21935  matsubgcell  21936  mamulid  21943  mamurid  21944  mattposcl  21955  mat1dimelbas  21973  mat1dimscm  21977  mat1dimmul  21978  m1detdiag  22099  mdetdiagid  22102  mdetunilem9  22122  pmatcoe1fsupp  22203  d1mat2pmat  22241  idcn  22761  hausdiag  23149  symgtgp  23610  ustref  23723  ustelimasn  23727  iducn  23788  ismet  23829  isxmet  23830  idnghm  24260  resubmet  24318  xrsxmet  24325  cphnm  24710  tcphnmval  24746  ipcau2  24751  tcphcphlem1  24752  tcphcphlem2  24753  tcphcph  24754  cmssmscld  24867  chordthmlem  26337  slerflex  27266  lrrecpo  27427  subsid  27540  divs1  27654  ismot  27817  hmoval  30094  htth  30202  hvsubid  30310  hvnegid  30311  hv2times  30345  hiidrcl  30379  normval  30408  issh2  30493  chjidm  30804  normcan  30860  ho2times  31103  kbpj  31240  lnop0  31250  riesz3i  31346  leoprf  31412  leopsq  31413  cvnref  31575  gtiso  31953  fldextid  32769  prsss  32927  deranglem  34188  elfix2  34907  linedegen  35146  filnetlem2  35312  bj-ru0  35871  matunitlindflem2  36533  matunitlindf  36534  ftc1anclem3  36611  prdsbnd2  36711  reheibor  36755  ismgmOLD  36766  opidon2OLD  36770  exidreslem  36793  rngo2  36823  opideq  37260  eldmcoss2  37377  2xp3dxp2ge1d  41070  sn-inelr  41386  mzpf  41522  acongrep  41767  ttac  41823  mendval  41973  iocinico  42009  iocmbl  42010  seff  43116  sblpnf  43117  sigarid  45622  cnambpcma  46050  2leaddle2  46054  clintopval  46662  2arymaptfv  47385  2arymaptfo  47388  itcoval2  47398  itcoval3  47399