Theorem pm2.61dne 3018

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 3015	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2932

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 207  df-ne 2933

This theorem is referenced by:  pm2.61dane  3019  wefrc  5648  wereu2  5651  frpomin  6329  oe0lem  8525  fisupg  9296  marypha1lem  9445  fiinfg  9513  wdomtr  9589  unxpwdom2  9602  frmin  9763  fpwwe2lem12  10656  grur1a  10833  grutsk  10836  fimaxre2  12187  xlesubadd  13279  cshwidxmod  14821  sqreu  15379  pcxnn0cl  16880  pcxcl  16881  pcmpt  16912  symggen  19451  isabvd  20772  lspprat  21114  mdetralt  22546  ordtrest2lem  23141  ordthauslem  23321  comppfsc  23470  fbssint  23776  fclscf  23963  tgptsmscld  24089  ovoliunnul  25460  itg11  25644  i1fadd  25648  fta1g  26127  plydiveu  26258  fta1  26268  mulcxp  26646  cxpsqrt  26664  ostth3  27601  madebdaylemlrcut  27862  brbtwn2  28884  colinearalg  28889  clwwisshclwws  29996  ordtrest2NEWlem  33953  subfacp1lem5  35206  btwnexch2  36041  fnemeet2  36385  fnejoin2  36387  limsucncmpi  36463  areacirc  37737  sstotbnd2  37798  ssbnd  37812  prdsbnd2  37819  rrncmslem  37856  atnlt  39331  atlelt  39457  llnnlt  39542  lplnnlt  39584  lvolnltN  39637  pmapglb2N  39790  pmapglb2xN  39791  paddasslem14  39852  cdleme27a  40386  sdomne0  43437  sdomne0d  43438  modelaxreplem1  45003  iccpartigtl  47437