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  2164  eqeq12d  2777  rru  3737  dedth2v  4545  dedth3v  4546  dedth4v  4547  disjprsn  4675  opidg  4852  unisng  4885  intsng  4943  isso2i  5596  poinxp  5732  posn  5737  xpid11  5914  dfpo2  6298  predpoirr  6335  predfrirr  6336  f1oprswap  6868  f1o2sn  7143  residpr  7144  f1mpt  7263  f1eqcocnv  7307  isopolem  7351  3xpexg  7764  sqxpexg  7767  poxp  8138  poxp2  8153  poxp3  8160  oe0  8523  oecl  8538  nnmsucr  8627  ecopover  8835  enrefg  9004  php  9215  3xpfi  9305  dffi3  9416  elirrv  9584  infxpenlem  10085  isfin5  10370  isfin5-2  10462  pwfseqlem4a  10739  pwfseqlem4  10740  pwfseqlem5  10741  pwfseq  10742  nqereu  11007  halfnq  11054  ltsopr  11110  1idsr  11176  00sr  11177  sqgt0sr  11184  leid  11399  msqgt0  11829  msqge0  11830  recextlem1  11939  recextlem2  11940  recex  11941  div1  11999  cju  12309  2halves  12557  msqznn  12774  xrltnr  13241  xrleid  13273  iccid  13514  m1expeven  14245  sqneg  14251  sqcl  14254  nnsqcl  14264  qsqcl  14266  expubnd  14314  bernneq  14366  faclbnd  14427  faclbnd3  14429  hashfac  14596  leiso  14597  cjmulval  15305  fallrisefac  16185  sin2t  16338  cos2t  16339  divalglem0  16556  divalglem2  16558  gcd0id  16684  lcmid  16777  lcmgcdeq  16780  lcmfsn  16803  isprm5  16876  prslem  18464  pslem  18739  dirref  18768  efmndbasabf  19061  efmndhash  19065  efmndbasfi  19066  efmnd1bas  19082  submefmnd  19084  sgrp2nmndlem4  19120  grpsubid  19227  grp1inv  19251  cntzi  19536  symgbasfi  19586  symg1bas  19598  pgrpsubgsymg  19616  symgextfve  19626  pmtrfinv  19668  psgnsn  19727  ipeq0  21937  matsca2  22728  matbas2  22729  matplusgcell  22741  matsubgcell  22742  mamulid  22749  mamurid  22750  mattposcl  22761  mat1dimelbas  22779  mat1dimscm  22783  mat1dimmul  22784  m1detdiag  22905  mdetdiagid  22908  mdetunilem9  22928  matunitlindflem2  22988  matunitlindf  22989  pmatcoe1fsupp  23012  d1mat2pmat  23050  idcn  23568  hausdiag  23957  symgtgp  24418  ustref  24531  ustelimasn  24535  iducn  24594  ismet  24635  isxmet  24636  idnghm  25055  resubmet  25114  xrsxmet  25122  cphnm  25507  tcphnmval  25543  ipcau2  25548  tcphcphlem1  25549  tcphcphlem2  25550  tcphcph  25551  cmssmscld  25664  chordthmlem  27153  lesid  28117  lrrecpo  28320  subsid  28448  divs1  28583  zsoring  28788  ismot  28991  hmoval  31405  htth  31513  hvsubid  31621  hvnegid  31622  hv2times  31656  hiidrcl  31690  normval  31719  issh2  31804  chjidm  32115  normcan  32171  ho2times  32414  kbpj  32551  lnop0  32561  riesz3i  32657  leoprf  32723  leopsq  32724  cvnref  32886  gtiso  33287  fldextid  34284  prsss  34541  fineqvnttrclse  35775  deranglem  35910  elfix2  36646  linedegen  36888  filnetlem2  37147  ftc1anclem3  38593  prdsbnd2  38709  reheibor  38753  ismgmOLD  38764  opidon2OLD  38768  exidreslem  38791  rngo2  38821  opideq  39255  eldmcoss2  39461  mzpf  43726  acongrep  43966  ttac  44022  mendval  44165  iocinico  44198  iocmbl  44199  seff  45278  sblpnf  45279  omhf  45999  sigarid  47837  cnambpcma  48333  2leaddle2  48337  grlicref  49079  clintopval  49270  2arymaptfv  49732  2arymaptfo  49735  itcoval2  49745  itcoval3  49746  resipos  50052  nelsubclem  50144  initoo2  50309  termoo2  50310  setc1onsubc  50679