Theorem anidms 389

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 113	. 2 ⊢ (𝜑 → (𝜑 → 𝜓))
3	2	pm2.43i 48	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106

This theorem is referenced by:  sylancb  409  sylancbr  410  intsng  3678  pwnss  3941  posng  4438  xpid11m  4585  resiexg  4683  f1mpt  5442  f1eqcocnv  5462  isopolem  5492  poxp  5884  nnmsucr  6132  erex  6196  ecopover  6270  ecopoverg  6273  enrefg  6311  ltsopi  6572  recexnq  6642  ltsonq  6650  ltaddnq  6659  nsmallnqq  6664  ltpopr  6847  ltposr  7002  1idsr  7007  00sr  7008  axltirr  7246  leid  7262  reapirr  7744  inelr  7751  apsqgt0  7768  apirr  7772  msqge0  7783  recextlem1  7808  recexaplem2  7809  recexap  7810  div1  7858  cju  8105  2halves  8327  msqznn  8528  xrltnr  8931  xrleid  8950  iooidg  9008  iccid  9024  m1expeven  9620  expubnd  9630  sqneg  9632  sqcl  9634  sqap0  9639  nnsqcl  9642  qsqcl  9644  subsq2  9679  bernneq  9690  faclbnd  9765  faclbnd3  9767  cjmulval  9913  gcd0id  10514  lcmid  10606  lcmgcdeq  10609  bj-snexg  10861