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  3989  pwnss  4278  posng  4829  sqxpexg  4875  xpid11  4987  resiexg  5090  f1mpt  5952  f1eqcocnv  5972  isopolem  6003  poxp  6443  nnmsucr  6736  erex  6806  ecopover  6882  ecopoverg  6885  enrefg  7018  3xpfi  7209  tapeq2  7585  netap  7586  2omotaplemap  7589  ltsopi  7653  recexnq  7723  ltsonq  7731  ltaddnq  7740  nsmallnqq  7745  ltpopr  7928  ltposr  8096  1idsr  8101  00sr  8102  axltirr  8358  leid  8375  reapirr  8871  inelr  8878  apsqgt0  8895  apirr  8899  msqge0  8910  recextlem1  8945  recexaplem2  8946  recexap  8947  msqap0  8962  div1  8999  cju  9257  2halves  9489  msqznn  9701  xrltnr  10136  xrleid  10157  iooidg  10266  iccid  10282  m1expeven  10977  expubnd  10987  sqneg  10989  sqcl  10991  sqap0  10997  nnsqcl  11000  qsqcl  11002  subsq2  11038  bernneq  11052  faclbnd  11133  faclbnd3  11135  cjmulval  11603  sin2t  12466  cos2t  12467  gcd0id  12706  lcmid  12808  lcmgcdeq  12811  intopsn  13636  mgm1  13639  sgrp1  13675  mnd1  13711  mnd1id  13712  grpsubid  13838  grp1  13860  grp1inv  13861  ringadd2  14277  ring1  14309  idcn  15208  ismet  15340  isxmet  15341  resubmet  15552  bj-snexg  16823