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  3956  pwnss  4242  posng  4790  sqxpexg  4834  xpid11  4946  resiexg  5049  f1mpt  5894  f1eqcocnv  5914  isopolem  5945  poxp  6376  nnmsucr  6632  erex  6702  ecopover  6778  ecopoverg  6781  enrefg  6913  3xpfi  7091  tapeq2  7435  netap  7436  2omotaplemap  7439  ltsopi  7503  recexnq  7573  ltsonq  7581  ltaddnq  7590  nsmallnqq  7595  ltpopr  7778  ltposr  7946  1idsr  7951  00sr  7952  axltirr  8209  leid  8226  reapirr  8720  inelr  8727  apsqgt0  8744  apirr  8748  msqge0  8759  recextlem1  8794  recexaplem2  8795  recexap  8796  div1  8846  cju  9104  2halves  9336  msqznn  9543  xrltnr  9971  xrleid  9992  iooidg  10101  iccid  10117  m1expeven  10803  expubnd  10813  sqneg  10815  sqcl  10817  sqap0  10823  nnsqcl  10826  qsqcl  10828  subsq2  10864  bernneq  10877  faclbnd  10958  faclbnd3  10960  cjmulval  11394  sin2t  12255  cos2t  12256  gcd0id  12495  lcmid  12597  lcmgcdeq  12600  intopsn  13395  mgm1  13398  sgrp1  13439  mnd1  13483  mnd1id  13484  grpsubid  13612  grp1  13634  grp1inv  13635  ringadd2  13985  ring1  14017  idcn  14880  ismet  15012  isxmet  15013  resubmet  15224  bj-snexg  16233