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  3957  pwnss  4243  posng  4791  sqxpexg  4835  xpid11  4947  resiexg  5050  f1mpt  5901  f1eqcocnv  5921  isopolem  5952  poxp  6384  nnmsucr  6642  erex  6712  ecopover  6788  ecopoverg  6791  enrefg  6923  3xpfi  7106  tapeq2  7450  netap  7451  2omotaplemap  7454  ltsopi  7518  recexnq  7588  ltsonq  7596  ltaddnq  7605  nsmallnqq  7610  ltpopr  7793  ltposr  7961  1idsr  7966  00sr  7967  axltirr  8224  leid  8241  reapirr  8735  inelr  8742  apsqgt0  8759  apirr  8763  msqge0  8774  recextlem1  8809  recexaplem2  8810  recexap  8811  div1  8861  cju  9119  2halves  9351  msqznn  9558  xrltnr  9987  xrleid  10008  iooidg  10117  iccid  10133  m1expeven  10820  expubnd  10830  sqneg  10832  sqcl  10834  sqap0  10840  nnsqcl  10843  qsqcl  10845  subsq2  10881  bernneq  10894  faclbnd  10975  faclbnd3  10977  cjmulval  11414  sin2t  12275  cos2t  12276  gcd0id  12515  lcmid  12617  lcmgcdeq  12620  intopsn  13415  mgm1  13418  sgrp1  13459  mnd1  13503  mnd1id  13504  grpsubid  13632  grp1  13654  grp1inv  13655  ringadd2  14005  ring1  14037  idcn  14901  ismet  15033  isxmet  15034  resubmet  15245  bj-snexg  16330