Theorem pm2.61dne 3049

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1508   ≠ wne 2962

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 199  df-ne 2963

This theorem is referenced by:  pm2.61dane  3050  wefrc  5398  wereu2  5401  oe0lem  7939  fisupg  8560  marypha1lem  8691  fiinfg  8757  wdomtr  8833  unxpwdom2  8846  fpwwe2lem13  9861  grur1a  10038  grutsk  10041  fimaxre2  11386  xlesubadd  12471  cshwidxmod  14026  sqreu  14580  pcxcl  16052  pcmpt  16083  symggen  18372  isabvd  19326  lspprat  19660  mdetralt  20937  ordtrest2lem  21531  ordthauslem  21711  comppfsc  21860  fbssint  22166  fclscf  22353  tgptsmscld  22478  ovoliunnul  23827  itg11  24011  i1fadd  24015  fta1g  24480  plydiveu  24606  fta1  24616  mulcxp  24985  cxpsqrt  25003  ostth3  25932  brbtwn2  26410  colinearalg  26415  clwwisshclwws  27546  ordtrest2NEWlem  30842  subfacp1lem5  32049  frpomin  32632  frmin  32638  btwnexch2  33038  fnemeet2  33269  fnejoin2  33271  limsucncmpi  33346  areacirc  34461  sstotbnd2  34527  ssbnd  34541  prdsbnd2  34548  rrncmslem  34585  atnlt  35927  atlelt  36052  llnnlt  36137  lplnnlt  36179  lvolnltN  36232  pmapglb2N  36385  pmapglb2xN  36386  paddasslem14  36447  cdleme27a  36981  iccpartigtl  42985