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  3983  pwnss  4272  posng  4822  sqxpexg  4868  xpid11  4980  resiexg  5083  f1mpt  5944  f1eqcocnv  5964  isopolem  5995  poxp  6428  nnmsucr  6721  erex  6791  ecopover  6867  ecopoverg  6870  enrefg  7003  3xpfi  7194  tapeq2  7567  netap  7568  2omotaplemap  7571  ltsopi  7635  recexnq  7705  ltsonq  7713  ltaddnq  7722  nsmallnqq  7727  ltpopr  7910  ltposr  8078  1idsr  8083  00sr  8084  axltirr  8340  leid  8357  reapirr  8851  inelr  8858  apsqgt0  8875  apirr  8879  msqge0  8890  recextlem1  8925  recexaplem2  8926  recexap  8927  div1  8977  cju  9235  2halves  9467  msqznn  9678  xrltnr  10112  xrleid  10133  iooidg  10242  iccid  10258  m1expeven  10948  expubnd  10958  sqneg  10960  sqcl  10962  sqap0  10968  nnsqcl  10971  qsqcl  10973  subsq2  11009  bernneq  11022  faclbnd  11103  faclbnd3  11105  cjmulval  11573  sin2t  12435  cos2t  12436  gcd0id  12675  lcmid  12777  lcmgcdeq  12780  intopsn  13580  mgm1  13583  sgrp1  13624  mnd1  13668  mnd1id  13669  grpsubid  13797  grp1  13819  grp1inv  13820  ringadd2  14171  ring1  14203  idcn  15077  ismet  15209  isxmet  15210  resubmet  15421  bj-snexg  16682