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  3924  pwnss  4210  posng  4754  sqxpexg  4798  xpid11  4909  resiexg  5012  f1mpt  5852  f1eqcocnv  5872  isopolem  5903  poxp  6330  nnmsucr  6586  erex  6656  ecopover  6732  ecopoverg  6735  enrefg  6867  3xpfi  7044  tapeq2  7380  netap  7381  2omotaplemap  7384  ltsopi  7448  recexnq  7518  ltsonq  7526  ltaddnq  7535  nsmallnqq  7540  ltpopr  7723  ltposr  7891  1idsr  7896  00sr  7897  axltirr  8154  leid  8171  reapirr  8665  inelr  8672  apsqgt0  8689  apirr  8693  msqge0  8704  recextlem1  8739  recexaplem2  8740  recexap  8741  div1  8791  cju  9049  2halves  9281  msqznn  9488  xrltnr  9916  xrleid  9937  iooidg  10046  iccid  10062  m1expeven  10748  expubnd  10758  sqneg  10760  sqcl  10762  sqap0  10768  nnsqcl  10771  qsqcl  10773  subsq2  10809  bernneq  10822  faclbnd  10903  faclbnd3  10905  cjmulval  11269  sin2t  12130  cos2t  12131  gcd0id  12370  lcmid  12472  lcmgcdeq  12475  intopsn  13269  mgm1  13272  sgrp1  13313  mnd1  13357  mnd1id  13358  grpsubid  13486  grp1  13508  grp1inv  13509  ringadd2  13859  ring1  13891  idcn  14754  ismet  14886  isxmet  14887  resubmet  15098  bj-snexg  15982