Theorem pm2.61dne 3021

Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
pm2.61dne.1	⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))
pm2.61dne.2	⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))

Assertion

Ref	Expression
pm2.61dne	⊢ (𝜑 → 𝜓)

Proof of Theorem pm2.61dne

Step	Hyp	Ref	Expression
1		pm2.61dne.2	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))
2		nne 2939	. . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)
3		pm2.61dne.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))
4	2, 3	syl5bi 245	. 2 ⊢ (𝜑 → (¬ 𝐴 ≠ 𝐵 → 𝜓))
5	1, 4	pm2.61d 182	1 ⊢ (𝜑 → 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1543   ≠ wne 2935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-ne 2936

This theorem is referenced by:  pm2.61dane  3022  wefrc  5534  wereu2  5537  frpomin  6183  oe0lem  8229  fisupg  8908  marypha1lem  9038  fiinfg  9104  wdomtr  9180  unxpwdom2  9193  frmin  9354  fpwwe2lem12  10239  grur1a  10416  grutsk  10419  fimaxre2  11760  xlesubadd  12836  cshwidxmod  14351  sqreu  14907  pcxnn0cl  16394  pcxcl  16395  pcmpt  16426  symggen  18834  isabvd  19828  lspprat  20162  mdetralt  21477  ordtrest2lem  22072  ordthauslem  22252  comppfsc  22401  fbssint  22707  fclscf  22894  tgptsmscld  23020  ovoliunnul  24376  itg11  24560  i1fadd  24564  fta1g  25037  plydiveu  25163  fta1  25173  mulcxp  25545  cxpsqrt  25563  ostth3  26491  brbtwn2  26968  colinearalg  26973  clwwisshclwws  28070  ordtrest2NEWlem  31558  subfacp1lem5  32831  madebdaylemlrcut  33773  btwnexch2  34019  fnemeet2  34250  fnejoin2  34252  limsucncmpi  34328  areacirc  35564  sstotbnd2  35626  ssbnd  35640  prdsbnd2  35647  rrncmslem  35684  atnlt  37021  atlelt  37146  llnnlt  37231  lplnnlt  37273  lvolnltN  37326  pmapglb2N  37479  pmapglb2xN  37480  paddasslem14  37541  cdleme27a  38075  iccpartigtl  44502