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  3908  pwnss  4192  posng  4735  sqxpexg  4779  xpid11  4889  resiexg  4991  f1mpt  5818  f1eqcocnv  5838  isopolem  5869  poxp  6290  nnmsucr  6546  erex  6616  ecopover  6692  ecopoverg  6695  enrefg  6823  3xpfi  6994  tapeq2  7320  netap  7321  2omotaplemap  7324  ltsopi  7387  recexnq  7457  ltsonq  7465  ltaddnq  7474  nsmallnqq  7479  ltpopr  7662  ltposr  7830  1idsr  7835  00sr  7836  axltirr  8093  leid  8110  reapirr  8604  inelr  8611  apsqgt0  8628  apirr  8632  msqge0  8643  recextlem1  8678  recexaplem2  8679  recexap  8680  div1  8730  cju  8988  2halves  9220  msqznn  9426  xrltnr  9854  xrleid  9875  iooidg  9984  iccid  10000  m1expeven  10678  expubnd  10688  sqneg  10690  sqcl  10692  sqap0  10698  nnsqcl  10701  qsqcl  10703  subsq2  10739  bernneq  10752  faclbnd  10833  faclbnd3  10835  cjmulval  11053  sin2t  11914  cos2t  11915  gcd0id  12146  lcmid  12248  lcmgcdeq  12251  intopsn  13010  mgm1  13013  sgrp1  13054  mnd1  13087  mnd1id  13088  grpsubid  13216  grp1  13238  grp1inv  13239  ringadd2  13583  ring1  13615  idcn  14448  ismet  14580  isxmet  14581  resubmet  14792  bj-snexg  15558