Theorem pm2.61dne 2868

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 2786	. . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)
3		pm2.61dne.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))
4	2, 3	syl5bi 231	. 2 ⊢ (𝜑 → (¬ 𝐴 ≠ 𝐵 → 𝜓))
5	1, 4	pm2.61d 169	1 ⊢ (𝜑 → 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ≠ wne 2780

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 196  df-ne 2782

This theorem is referenced by:  pm2.61dane  2869  wefrc  5032  wereu2  5035  oe0lem  7480  fisupg  8093  marypha1lem  8222  fiinfg  8288  wdomtr  8363  unxpwdom2  8376  fpwwe2lem13  9343  grur1a  9520  grutsk  9523  fimaxre2  10848  xlesubadd  11965  cshwidxmod  13400  sqreu  13948  pcxcl  15403  pcmpt  15434  symggen  17713  isabvd  18643  lspprat  18974  mdetralt  20233  ordtrest2lem  20817  ordthauslem  20997  comppfsc  21145  fbssint  21452  fclscf  21639  tgptsmscld  21764  ovoliunnul  23082  itg11  23264  i1fadd  23268  fta1g  23731  plydiveu  23857  fta1  23867  mulcxp  24231  cxpsqrt  24249  ostth3  25127  brbtwn2  25585  colinearalg  25590  clwwisshclww  26335  ordtrest2NEWlem  29296  subfacp1lem5  30420  frmin  30983  btwnexch2  31300  fnemeet2  31532  fnejoin2  31534  limsucncmpi  31614  areacirc  32675  sstotbnd2  32743  ssbnd  32757  prdsbnd2  32764  rrncmslem  32801  atnlt  33618  atlelt  33742  llnnlt  33827  lplnnlt  33869  lvolnltN  33922  pmapglb2N  34075  pmapglb2xN  34076  paddasslem14  34137  cdleme27a  34673  iccpartigtl  39961  clwwisshclwws  41235