Theorem pm2.61dne 3028

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

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

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 2941

This theorem is referenced by:  pm2.61dane  3029  wefrc  5679  wereu2  5682  frpomin  6361  oe0lem  8551  fisupg  9324  marypha1lem  9473  fiinfg  9539  wdomtr  9615  unxpwdom2  9628  frmin  9789  fpwwe2lem12  10682  grur1a  10859  grutsk  10862  fimaxre2  12213  xlesubadd  13305  cshwidxmod  14841  sqreu  15399  pcxnn0cl  16898  pcxcl  16899  pcmpt  16930  symggen  19488  isabvd  20813  lspprat  21155  mdetralt  22614  ordtrest2lem  23211  ordthauslem  23391  comppfsc  23540  fbssint  23846  fclscf  24033  tgptsmscld  24159  ovoliunnul  25542  itg11  25726  i1fadd  25730  fta1g  26209  plydiveu  26340  fta1  26350  mulcxp  26727  cxpsqrt  26745  ostth3  27682  madebdaylemlrcut  27937  brbtwn2  28920  colinearalg  28925  clwwisshclwws  30034  ordtrest2NEWlem  33921  subfacp1lem5  35189  btwnexch2  36024  fnemeet2  36368  fnejoin2  36370  limsucncmpi  36446  areacirc  37720  sstotbnd2  37781  ssbnd  37795  prdsbnd2  37802  rrncmslem  37839  atnlt  39314  atlelt  39440  llnnlt  39525  lplnnlt  39567  lvolnltN  39620  pmapglb2N  39773  pmapglb2xN  39774  paddasslem14  39835  cdleme27a  40369  sdomne0  43426  sdomne0d  43427  modelaxreplem1  44995  iccpartigtl  47410