Theorem anidms 395

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  sylancb  416  sylancbr  417  intsng  3865  pwnss  4145  posng  4683  sqxpexg  4727  xpid11  4834  resiexg  4936  f1mpt  5750  f1eqcocnv  5770  isopolem  5801  poxp  6211  nnmsucr  6467  erex  6537  ecopover  6611  ecopoverg  6614  enrefg  6742  3xpfi  6908  ltsopi  7282  recexnq  7352  ltsonq  7360  ltaddnq  7369  nsmallnqq  7374  ltpopr  7557  ltposr  7725  1idsr  7730  00sr  7731  axltirr  7986  leid  8003  reapirr  8496  inelr  8503  apsqgt0  8520  apirr  8524  msqge0  8535  recextlem1  8569  recexaplem2  8570  recexap  8571  div1  8620  cju  8877  2halves  9107  msqznn  9312  xrltnr  9736  xrleid  9757  iooidg  9866  iccid  9882  m1expeven  10523  expubnd  10533  sqneg  10535  sqcl  10537  sqap0  10542  nnsqcl  10545  qsqcl  10547  subsq2  10583  bernneq  10596  faclbnd  10675  faclbnd3  10677  cjmulval  10852  sin2t  11712  cos2t  11713  gcd0id  11934  lcmid  12034  lcmgcdeq  12037  intopsn  12621  mgm1  12624  sgrp1  12651  mnd1  12679  mnd1id  12680  idcn  13006  ismet  13138  isxmet  13139  resubmet  13342  bj-snexg  13947