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  5626  wereu2  5629  frpomin  6306  oe0lem  8450  fisupg  9200  marypha1lem  9348  fiinfg  9416  wdomtr  9492  unxpwdom2  9505  frmin  9673  fpwwe2lem12  10565  grur1a  10742  grutsk  10745  fimaxre2  12099  xlesubadd  13190  cshwidxmod  14738  sqreu  15296  pcxnn0cl  16800  pcxcl  16801  pcmpt  16832  symggen  19411  isabvd  20757  lspprat  21120  mdetralt  22564  ordtrest2lem  23159  ordthauslem  23339  comppfsc  23488  fbssint  23794  fclscf  23981  tgptsmscld  24107  ovoliunnul  25476  itg11  25660  i1fadd  25664  fta1g  26143  plydiveu  26274  fta1  26284  mulcxp  26662  cxpsqrt  26680  ostth3  27617  madebdaylemlrcut  27907  brbtwn2  28990  colinearalg  28995  clwwisshclwws  30102  ordtrest2NEWlem  34100  fissorduni  35267  subfacp1lem5  35400  btwnexch2  36239  fnemeet2  36583  fnejoin2  36585  limsucncmpi  36661  areacirc  37964  sstotbnd2  38025  ssbnd  38039  prdsbnd2  38046  rrncmslem  38083  atnlt  39689  atlelt  39814  llnnlt  39899  lplnnlt  39941  lvolnltN  39994  pmapglb2N  40147  pmapglb2xN  40148  paddasslem14  40209  cdleme27a  40743  sdomne0  43769  sdomne0d  43770  modelaxreplem1  45334  iccpartigtl  47783