Theorem pm2.61dne 3025

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

Syntax hints:   → wi 4   = wceq 1536   ≠ wne 2937

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 2938

This theorem is referenced by:  pm2.61dane  3026  wefrc  5682  wereu2  5685  frpomin  6362  oe0lem  8549  fisupg  9321  marypha1lem  9470  fiinfg  9536  wdomtr  9612  unxpwdom2  9625  frmin  9786  fpwwe2lem12  10679  grur1a  10856  grutsk  10859  fimaxre2  12210  xlesubadd  13301  cshwidxmod  14837  sqreu  15395  pcxnn0cl  16893  pcxcl  16894  pcmpt  16925  symggen  19502  isabvd  20829  lspprat  21172  mdetralt  22629  ordtrest2lem  23226  ordthauslem  23406  comppfsc  23555  fbssint  23861  fclscf  24048  tgptsmscld  24174  ovoliunnul  25555  itg11  25739  i1fadd  25743  fta1g  26223  plydiveu  26354  fta1  26364  mulcxp  26741  cxpsqrt  26759  ostth3  27696  madebdaylemlrcut  27951  brbtwn2  28934  colinearalg  28939  clwwisshclwws  30043  ordtrest2NEWlem  33882  subfacp1lem5  35168  btwnexch2  36004  fnemeet2  36349  fnejoin2  36351  limsucncmpi  36427  areacirc  37699  sstotbnd2  37760  ssbnd  37774  prdsbnd2  37781  rrncmslem  37818  atnlt  39294  atlelt  39420  llnnlt  39505  lplnnlt  39547  lvolnltN  39600  pmapglb2N  39753  pmapglb2xN  39754  paddasslem14  39815  cdleme27a  40349  sdomne0  43402  sdomne0d  43403  modelaxreplem1  44942  iccpartigtl  47347