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  4296  posng  4847  sqxpexg  4893  xpid11  5005  resiexg  5108  f1mpt  5977  f1eqcocnv  5997  isopolem  6028  poxp  6468  nnmsucr  6761  erex  6831  ecopover  6907  ecopoverg  6910  enrefg  7050  3xpfi  7241  tapeq2  7620  netap  7621  2omotaplemap  7624  ltsopi  7688  recexnq  7758  ltsonq  7766  ltaddnq  7775  nsmallnqq  7780  ltpopr  7963  ltposr  8131  1idsr  8136  00sr  8137  axltirr  8393  leid  8410  reapirr  8908  inelr  8915  apsqgt0  8932  apirr  8936  msqge0  8947  recextlem1  8982  recexaplem2  8983  recexap  8984  msqap0  8999  div1  9036  cju  9294  2halves  9539  msqznn  9751  xrltnr  10192  xrleid  10213  iooidg  10322  iccid  10338  m1expeven  11038  expubnd  11048  sqneg  11050  sqcl  11052  sqap0  11058  nnsqcl  11061  qsqcl  11063  subsq2  11099  bernneq  11113  faclbnd  11195  faclbnd3  11197  hashfac  11304  cjmulval  11669  sin2t  12535  cos2t  12536  gcd0id  12775  lcmid  12877  lcmgcdeq  12880  intopsn  13740  mgm1  13743  sgrp1  13779  mnd1  13815  mnd1id  13816  grpsubid  13942  grp1  13964  grp1inv  13965  cntzi  14156  ringadd2  14416  ring1  14448  idcn  15404  ismet  15536  isxmet  15537  resubmet  15748  bj-snexg  17104