Theorem pm2.61dne 3019

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

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

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 2934

This theorem is referenced by:  pm2.61dane  3020  wefrc  5619  wereu2  5622  frpomin  6299  oe0lem  8442  fisupg  9192  marypha1lem  9340  fiinfg  9408  wdomtr  9484  unxpwdom2  9497  frmin  9667  fpwwe2lem12  10559  grur1a  10736  grutsk  10739  fimaxre2  12095  xlesubadd  13209  cshwidxmod  14759  sqreu  15317  pcxnn0cl  16825  pcxcl  16826  pcmpt  16857  symggen  19439  isabvd  20783  lspprat  21146  mdetralt  22586  ordtrest2lem  23181  ordthauslem  23361  comppfsc  23510  fbssint  23816  fclscf  24003  tgptsmscld  24129  ovoliunnul  25487  itg11  25671  i1fadd  25675  fta1g  26148  plydiveu  26278  fta1  26288  mulcxp  26665  cxpsqrt  26683  ostth3  27618  madebdaylemlrcut  27908  brbtwn2  28991  colinearalg  28996  clwwisshclwws  30103  ordtrest2NEWlem  34085  fissorduni  35252  subfacp1lem5  35385  btwnexch2  36224  fnemeet2  36568  fnejoin2  36570  limsucncmpi  36646  areacirc  38051  sstotbnd2  38112  ssbnd  38126  prdsbnd2  38133  rrncmslem  38170  atnlt  39776  atlelt  39901  llnnlt  39986  lplnnlt  40028  lvolnltN  40081  pmapglb2N  40234  pmapglb2xN  40235  paddasslem14  40296  cdleme27a  40830  sdomne0  43861  sdomne0d  43862  modelaxreplem1  45426  iccpartigtl  47898