Theorem anidms 397

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 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  sylancb  418  sylancbr  419  intsng  3967  pwnss  4255  posng  4804  sqxpexg  4849  xpid11  4961  resiexg  5064  f1mpt  5922  f1eqcocnv  5942  isopolem  5973  poxp  6406  nnmsucr  6699  erex  6769  ecopover  6845  ecopoverg  6848  enrefg  6980  3xpfi  7169  tapeq2  7515  netap  7516  2omotaplemap  7519  ltsopi  7583  recexnq  7653  ltsonq  7661  ltaddnq  7670  nsmallnqq  7675  ltpopr  7858  ltposr  8026  1idsr  8031  00sr  8032  axltirr  8288  leid  8305  reapirr  8799  inelr  8806  apsqgt0  8823  apirr  8827  msqge0  8838  recextlem1  8873  recexaplem2  8874  recexap  8875  div1  8925  cju  9183  2halves  9415  msqznn  9624  xrltnr  10058  xrleid  10079  iooidg  10188  iccid  10204  m1expeven  10894  expubnd  10904  sqneg  10906  sqcl  10908  sqap0  10914  nnsqcl  10917  qsqcl  10919  subsq2  10955  bernneq  10968  faclbnd  11049  faclbnd3  11051  cjmulval  11511  sin2t  12373  cos2t  12374  gcd0id  12613  lcmid  12715  lcmgcdeq  12718  intopsn  13513  mgm1  13516  sgrp1  13557  mnd1  13601  mnd1id  13602  grpsubid  13730  grp1  13752  grp1inv  13753  ringadd2  14104  ring1  14136  idcn  15006  ismet  15138  isxmet  15139  resubmet  15350  bj-snexg  16611