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  3880  pwnss  4161  posng  4700  sqxpexg  4744  xpid11  4852  resiexg  4954  f1mpt  5774  f1eqcocnv  5794  isopolem  5825  poxp  6235  nnmsucr  6491  erex  6561  ecopover  6635  ecopoverg  6638  enrefg  6766  3xpfi  6932  tapeq2  7254  netap  7255  2omotaplemap  7258  ltsopi  7321  recexnq  7391  ltsonq  7399  ltaddnq  7408  nsmallnqq  7413  ltpopr  7596  ltposr  7764  1idsr  7769  00sr  7770  axltirr  8026  leid  8043  reapirr  8536  inelr  8543  apsqgt0  8560  apirr  8564  msqge0  8575  recextlem1  8610  recexaplem2  8611  recexap  8612  div1  8662  cju  8920  2halves  9150  msqznn  9355  xrltnr  9781  xrleid  9802  iooidg  9911  iccid  9927  m1expeven  10569  expubnd  10579  sqneg  10581  sqcl  10583  sqap0  10589  nnsqcl  10592  qsqcl  10594  subsq2  10630  bernneq  10643  faclbnd  10723  faclbnd3  10725  cjmulval  10899  sin2t  11759  cos2t  11760  gcd0id  11982  lcmid  12082  lcmgcdeq  12085  intopsn  12791  mgm1  12794  sgrp1  12821  mnd1  12852  mnd1id  12853  grpsubid  12959  grp1  12981  grp1inv  12982  ringadd2  13215  ring1  13241  idcn  13797  ismet  13929  isxmet  13930  resubmet  14133  bj-snexg  14749