Theorem pm2.61dne 3028

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.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))
2	1	com12 32	. 2 ⊢ (𝐴 = 𝐵 → (𝜑 → 𝜓))
3		pm2.61dne.2	. . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))
4	3	com12 32	. 2 ⊢ (𝐴 ≠ 𝐵 → (𝜑 → 𝜓))
5	2, 4	pm2.61ine 3025	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2940

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 206  df-ne 2941

This theorem is referenced by:  pm2.61dane  3029  wefrc  5670  wereu2  5673  frpomin  6341  oe0lem  8515  fisupg  9293  marypha1lem  9430  fiinfg  9496  wdomtr  9572  unxpwdom2  9585  frmin  9746  fpwwe2lem12  10639  grur1a  10816  grutsk  10819  fimaxre2  12161  xlesubadd  13244  cshwidxmod  14755  sqreu  15309  pcxnn0cl  16795  pcxcl  16796  pcmpt  16827  symggen  19340  isabvd  20432  lspprat  20772  mdetralt  22117  ordtrest2lem  22714  ordthauslem  22894  comppfsc  23043  fbssint  23349  fclscf  23536  tgptsmscld  23662  ovoliunnul  25031  itg11  25215  i1fadd  25219  fta1g  25692  plydiveu  25818  fta1  25828  mulcxp  26200  cxpsqrt  26218  ostth3  27148  madebdaylemlrcut  27401  brbtwn2  28201  colinearalg  28206  clwwisshclwws  29306  ordtrest2NEWlem  32971  subfacp1lem5  34244  btwnexch2  35064  fnemeet2  35338  fnejoin2  35340  limsucncmpi  35416  areacirc  36667  sstotbnd2  36728  ssbnd  36742  prdsbnd2  36749  rrncmslem  36786  atnlt  38269  atlelt  38395  llnnlt  38480  lplnnlt  38522  lvolnltN  38575  pmapglb2N  38728  pmapglb2xN  38729  paddasslem14  38790  cdleme27a  39324  sdomne0  42246  sdomne0d  42247  iccpartigtl  46170