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  7619  netap  7620  2omotaplemap  7623  ltsopi  7687  recexnq  7757  ltsonq  7765  ltaddnq  7774  nsmallnqq  7779  ltpopr  7962  ltposr  8130  1idsr  8135  00sr  8136  axltirr  8392  leid  8409  reapirr  8907  inelr  8914  apsqgt0  8931  apirr  8935  msqge0  8946  recextlem1  8981  recexaplem2  8982  recexap  8983  msqap0  8998  div1  9035  cju  9293  2halves  9538  msqznn  9750  xrltnr  10191  xrleid  10212  iooidg  10321  iccid  10337  m1expeven  11036  expubnd  11046  sqneg  11048  sqcl  11050  sqap0  11056  nnsqcl  11059  qsqcl  11061  subsq2  11097  bernneq  11111  faclbnd  11193  faclbnd3  11195  hashfac  11302  cjmulval  11667  sin2t  12532  cos2t  12533  gcd0id  12772  lcmid  12874  lcmgcdeq  12877  intopsn  13736  mgm1  13739  sgrp1  13775  mnd1  13811  mnd1id  13812  grpsubid  13938  grp1  13960  grp1inv  13961  ringadd2  14381  ring1  14413  idcn  15362  ismet  15494  isxmet  15495  resubmet  15706  bj-snexg  17036