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  3960  pwnss  4247  posng  4796  sqxpexg  4841  xpid11  4953  resiexg  5056  f1mpt  5907  f1eqcocnv  5927  isopolem  5958  poxp  6392  nnmsucr  6651  erex  6721  ecopover  6797  ecopoverg  6800  enrefg  6932  3xpfi  7118  tapeq2  7462  netap  7463  2omotaplemap  7466  ltsopi  7530  recexnq  7600  ltsonq  7608  ltaddnq  7617  nsmallnqq  7622  ltpopr  7805  ltposr  7973  1idsr  7978  00sr  7979  axltirr  8236  leid  8253  reapirr  8747  inelr  8754  apsqgt0  8771  apirr  8775  msqge0  8786  recextlem1  8821  recexaplem2  8822  recexap  8823  div1  8873  cju  9131  2halves  9363  msqznn  9570  xrltnr  10004  xrleid  10025  iooidg  10134  iccid  10150  m1expeven  10838  expubnd  10848  sqneg  10850  sqcl  10852  sqap0  10858  nnsqcl  10861  qsqcl  10863  subsq2  10899  bernneq  10912  faclbnd  10993  faclbnd3  10995  cjmulval  11439  sin2t  12300  cos2t  12301  gcd0id  12540  lcmid  12642  lcmgcdeq  12645  intopsn  13440  mgm1  13443  sgrp1  13484  mnd1  13528  mnd1id  13529  grpsubid  13657  grp1  13679  grp1inv  13680  ringadd2  14030  ring1  14062  idcn  14926  ismet  15058  isxmet  15059  resubmet  15270  bj-snexg  16443