Theorem pm2.61dne 3014

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

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

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 2929

This theorem is referenced by:  pm2.61dane  3015  wefrc  5608  wereu2  5611  frpomin  6287  oe0lem  8428  fisupg  9172  marypha1lem  9317  fiinfg  9385  wdomtr  9461  unxpwdom2  9474  frmin  9642  fpwwe2lem12  10533  grur1a  10710  grutsk  10713  fimaxre2  12067  xlesubadd  13162  cshwidxmod  14710  sqreu  15268  pcxnn0cl  16772  pcxcl  16773  pcmpt  16804  symggen  19382  isabvd  20727  lspprat  21090  mdetralt  22523  ordtrest2lem  23118  ordthauslem  23298  comppfsc  23447  fbssint  23753  fclscf  23940  tgptsmscld  24066  ovoliunnul  25435  itg11  25619  i1fadd  25623  fta1g  26102  plydiveu  26233  fta1  26243  mulcxp  26621  cxpsqrt  26639  ostth3  27576  madebdaylemlrcut  27844  brbtwn2  28883  colinearalg  28888  clwwisshclwws  29995  ordtrest2NEWlem  33935  fissorduni  35101  subfacp1lem5  35228  btwnexch2  36065  fnemeet2  36409  fnejoin2  36411  limsucncmpi  36487  areacirc  37761  sstotbnd2  37822  ssbnd  37836  prdsbnd2  37843  rrncmslem  37880  atnlt  39360  atlelt  39485  llnnlt  39570  lplnnlt  39612  lvolnltN  39665  pmapglb2N  39818  pmapglb2xN  39819  paddasslem14  39880  cdleme27a  40414  sdomne0  43454  sdomne0d  43455  modelaxreplem1  45019  iccpartigtl  47462