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  3896  pwnss  4180  posng  4719  sqxpexg  4763  xpid11  4871  resiexg  4973  f1mpt  5796  f1eqcocnv  5816  isopolem  5847  poxp  6261  nnmsucr  6517  erex  6587  ecopover  6663  ecopoverg  6666  enrefg  6794  3xpfi  6963  tapeq2  7287  netap  7288  2omotaplemap  7291  ltsopi  7354  recexnq  7424  ltsonq  7432  ltaddnq  7441  nsmallnqq  7446  ltpopr  7629  ltposr  7797  1idsr  7802  00sr  7803  axltirr  8060  leid  8077  reapirr  8570  inelr  8577  apsqgt0  8594  apirr  8598  msqge0  8609  recextlem1  8644  recexaplem2  8645  recexap  8646  div1  8696  cju  8954  2halves  9184  msqznn  9389  xrltnr  9816  xrleid  9837  iooidg  9946  iccid  9962  m1expeven  10608  expubnd  10618  sqneg  10620  sqcl  10622  sqap0  10628  nnsqcl  10631  qsqcl  10633  subsq2  10669  bernneq  10682  faclbnd  10763  faclbnd3  10765  cjmulval  10939  sin2t  11799  cos2t  11800  gcd0id  12022  lcmid  12124  lcmgcdeq  12127  intopsn  12855  mgm1  12858  sgrp1  12898  mnd1  12931  mnd1id  12932  grpsubid  13052  grp1  13074  grp1inv  13075  ringadd2  13407  ring1  13437  idcn  14198  ismet  14330  isxmet  14331  resubmet  14534  bj-snexg  15168