Theorem pm2.61dne 3029

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

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2941

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 2942

This theorem is referenced by:  pm2.61dane  3030  wefrc  5671  wereu2  5674  frpomin  6342  oe0lem  8513  fisupg  9291  marypha1lem  9428  fiinfg  9494  wdomtr  9570  unxpwdom2  9583  frmin  9744  fpwwe2lem12  10637  grur1a  10814  grutsk  10817  fimaxre2  12159  xlesubadd  13242  cshwidxmod  14753  sqreu  15307  pcxnn0cl  16793  pcxcl  16794  pcmpt  16825  symggen  19338  isabvd  20428  lspprat  20766  mdetralt  22110  ordtrest2lem  22707  ordthauslem  22887  comppfsc  23036  fbssint  23342  fclscf  23529  tgptsmscld  23655  ovoliunnul  25024  itg11  25208  i1fadd  25212  fta1g  25685  plydiveu  25811  fta1  25821  mulcxp  26193  cxpsqrt  26211  ostth3  27141  madebdaylemlrcut  27393  brbtwn2  28163  colinearalg  28168  clwwisshclwws  29268  ordtrest2NEWlem  32902  subfacp1lem5  34175  btwnexch2  34995  fnemeet2  35252  fnejoin2  35254  limsucncmpi  35330  areacirc  36581  sstotbnd2  36642  ssbnd  36656  prdsbnd2  36663  rrncmslem  36700  atnlt  38183  atlelt  38309  llnnlt  38394  lplnnlt  38436  lvolnltN  38489  pmapglb2N  38642  pmapglb2xN  38643  paddasslem14  38704  cdleme27a  39238  sdomne0  42164  sdomne0d  42165  iccpartigtl  46091