Theorem pm2.61dne 3042

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

Syntax hints:   → wi 4   = wceq 1568   ≠ wne 2956

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 210  df-ne 2957

This theorem is referenced by:  pm2.61dane  3043  wefrc  5655  wereu2  5658  frpomin  6341  oe0lem  8497  fisupg  9247  marypha1lem  9392  fiinfg  9460  wdomtr  9536  unxpwdom2  9549  frmin  9720  fpwwe2lem12  10626  grur1a  10803  grutsk  10806  fimaxre2  12159  xlesubadd  13288  cshwidxmod  14839  sqreu  15411  pcxnn0cl  16919  pcxcl  16920  pcmpt  16951  symggen  19539  isabvd  20894  lspprat  21256  mdetralt  22744  ordtrest2lem  23339  ordthauslem  23519  comppfsc  23668  fbssint  23974  fclscf  24161  tgptsmscld  24287  ovoliunnul  25645  itg11  25829  i1fadd  25833  fta1g  26306  plydiveu  26438  fta1  26448  mulcxp  26826  cxpsqrt  26844  ostth3  27778  madebdaylemlrcut  28068  brbtwn2  29221  colinearalg  29226  clwwisshclwws  30332  ordtrest2NEWlem  34278  fissorduni  35444  subfacp1lem5  35630  btwnexch2  36469  fnemeet2  36822  fnejoin2  36824  limsucncmpi  36900  areacirc  38308  sstotbnd2  38369  ssbnd  38383  prdsbnd2  38390  rrncmslem  38427  atnlt  40033  atlelt  40158  llnnlt  40243  lplnnlt  40285  lvolnltN  40338  pmapglb2N  40491  pmapglb2xN  40492  paddasslem14  40553  cdleme27a  41087  sdomne0  44087  sdomne0d  44088  modelaxreplem1  45635  iccpartigtl  48117