Theorem pm2.61dne 3043

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

Syntax hints:   → wi 4   = wceq 1560   ≠ wne 2957

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 209  df-ne 2958

This theorem is referenced by:  pm2.61dane  3044  wefrc  5641  wereu2  5644  frpomin  6327  oe0lem  8482  fisupg  9232  marypha1lem  9379  fiinfg  9447  wdomtr  9523  unxpwdom2  9536  frmin  9707  fpwwe2lem12  10600  grur1a  10777  grutsk  10780  fimaxre2  12137  xlesubadd  13266  cshwidxmod  14816  sqreu  15388  pcxnn0cl  16896  pcxcl  16897  pcmpt  16928  symggen  19510  isabvd  20858  lspprat  21220  mdetralt  22665  ordtrest2lem  23260  ordthauslem  23440  comppfsc  23589  fbssint  23895  fclscf  24082  tgptsmscld  24208  ovoliunnul  25566  itg11  25750  i1fadd  25754  fta1g  26227  plydiveu  26359  fta1  26369  mulcxp  26747  cxpsqrt  26765  ostth3  27699  madebdaylemlrcut  27989  brbtwn2  29103  colinearalg  29108  clwwisshclwws  30214  ordtrest2NEWlem  34216  fissorduni  35382  subfacp1lem5  35531  btwnexch2  36370  fnemeet2  36724  fnejoin2  36726  limsucncmpi  36802  areacirc  38209  sstotbnd2  38270  ssbnd  38284  prdsbnd2  38291  rrncmslem  38328  atnlt  39934  atlelt  40059  llnnlt  40144  lplnnlt  40186  lvolnltN  40239  pmapglb2N  40392  pmapglb2xN  40393  paddasslem14  40454  cdleme27a  40988  sdomne0  43986  sdomne0d  43987  modelaxreplem1  45551  iccpartigtl  48026