Theorem anidms 401

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  sylancb  422  sylancbr  423  intsng  4004  pwnss  4298  posng  4849  sqxpexg  4895  xpid11  5007  resiexg  5111  f1mpt  5980  f1eqcocnv  6000  isopolem  6031  poxp  6472  nnmsucr  6765  erex  6835  ecopover  6911  ecopoverg  6914  enrefg  7054  3xpfi  7245  tapeq2  7625  netap  7626  2omotaplemap  7629  ltsopi  7693  recexnq  7763  ltsonq  7771  ltaddnq  7780  nsmallnqq  7785  ltpopr  7968  ltposr  8136  1idsr  8141  00sr  8142  axltirr  8398  leid  8415  reapirr  8913  inelr  8920  apsqgt0  8937  apirr  8941  msqge0  8952  recextlem1  8987  recexaplem2  8988  recexap  8989  msqap0  9004  div1  9041  cju  9299  2halves  9545  msqznn  9757  xrltnr  10198  xrleid  10219  iooidg  10328  iccid  10344  m1expeven  11044  expubnd  11054  sqneg  11056  sqcl  11058  sqap0  11064  nnsqcl  11067  qsqcl  11069  subsq2  11105  bernneq  11119  faclbnd  11201  faclbnd3  11203  hashfac  11310  cjmulval  11675  sin2t  12541  cos2t  12542  gcd0id  12781  lcmid  12883  lcmgcdeq  12886  intopsn  13746  mgm1  13749  sgrp1  13785  mnd1  13821  mnd1id  13822  grpsubid  13948  grp1  13970  grp1inv  13971  cntzi  14162  ringadd2  14439  ring1  14471  idcn  15438  ismet  15570  isxmet  15571  resubmet  15782  bj-snexg  17143