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  27425  subsid  27537  divs1  27651  ismot  27786  hmoval  30063  htth  30171  hvsubid  30279  hvnegid  30280  hv2times  30314  hiidrcl  30348  normval  30377  issh2  30462  chjidm  30773  normcan  30829  ho2times  31072  kbpj  31209  lnop0  31219  riesz3i  31315  leoprf  31381  leopsq  31382  cvnref  31544  gtiso  31922  fldextid  32738  prsss  32896  deranglem  34157  elfix2  34876  linedegen  35115  filnetlem2  35264  bj-ru0  35823  matunitlindflem2  36485  matunitlindf  36486  ftc1anclem3  36563  prdsbnd2  36663  reheibor  36707  ismgmOLD  36718  opidon2OLD  36722  exidreslem  36745  rngo2  36775  opideq  37212  eldmcoss2  37329  2xp3dxp2ge1d  41022  sn-inelr  41338  mzpf  41474  acongrep  41719  ttac  41775  mendval  41925  iocinico  41961  iocmbl  41962  seff  43068  sblpnf  43069  sigarid  45574  cnambpcma  46002  2leaddle2  46006  clintopval  46614  2arymaptfv  47337  2arymaptfo  47340  itcoval2  47350  itcoval3  47351