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  3909  pwnss  4193  posng  4736  sqxpexg  4780  xpid11  4890  resiexg  4992  f1mpt  5821  f1eqcocnv  5841  isopolem  5872  poxp  6299  nnmsucr  6555  erex  6625  ecopover  6701  ecopoverg  6704  enrefg  6832  3xpfi  7003  tapeq2  7338  netap  7339  2omotaplemap  7342  ltsopi  7406  recexnq  7476  ltsonq  7484  ltaddnq  7493  nsmallnqq  7498  ltpopr  7681  ltposr  7849  1idsr  7854  00sr  7855  axltirr  8112  leid  8129  reapirr  8623  inelr  8630  apsqgt0  8647  apirr  8651  msqge0  8662  recextlem1  8697  recexaplem2  8698  recexap  8699  div1  8749  cju  9007  2halves  9239  msqznn  9445  xrltnr  9873  xrleid  9894  iooidg  10003  iccid  10019  m1expeven  10697  expubnd  10707  sqneg  10709  sqcl  10711  sqap0  10717  nnsqcl  10720  qsqcl  10722  subsq2  10758  bernneq  10771  faclbnd  10852  faclbnd3  10854  cjmulval  11072  sin2t  11933  cos2t  11934  gcd0id  12173  lcmid  12275  lcmgcdeq  12278  intopsn  13071  mgm1  13074  sgrp1  13115  mnd1  13159  mnd1id  13160  grpsubid  13288  grp1  13310  grp1inv  13311  ringadd2  13661  ring1  13693  idcn  14556  ismet  14688  isxmet  14689  resubmet  14900  bj-snexg  15666