Theorem pm2.61dne 3016

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

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

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 2931

This theorem is referenced by:  pm2.61dane  3017  wefrc  5616  wereu2  5619  frpomin  6296  oe0lem  8438  fisupg  9186  marypha1lem  9334  fiinfg  9402  wdomtr  9478  unxpwdom2  9491  frmin  9659  fpwwe2lem12  10551  grur1a  10728  grutsk  10731  fimaxre2  12085  xlesubadd  13176  cshwidxmod  14724  sqreu  15282  pcxnn0cl  16786  pcxcl  16787  pcmpt  16818  symggen  19397  isabvd  20743  lspprat  21106  mdetralt  22550  ordtrest2lem  23145  ordthauslem  23325  comppfsc  23474  fbssint  23780  fclscf  23967  tgptsmscld  24093  ovoliunnul  25462  itg11  25646  i1fadd  25650  fta1g  26129  plydiveu  26260  fta1  26270  mulcxp  26648  cxpsqrt  26666  ostth3  27603  madebdaylemlrcut  27871  brbtwn2  28927  colinearalg  28932  clwwisshclwws  30039  ordtrest2NEWlem  34028  fissorduni  35195  subfacp1lem5  35327  btwnexch2  36166  fnemeet2  36510  fnejoin2  36512  limsucncmpi  36588  areacirc  37853  sstotbnd2  37914  ssbnd  37928  prdsbnd2  37935  rrncmslem  37972  atnlt  39512  atlelt  39637  llnnlt  39722  lplnnlt  39764  lvolnltN  39817  pmapglb2N  39970  pmapglb2xN  39971  paddasslem14  40032  cdleme27a  40566  sdomne0  43596  sdomne0d  43597  modelaxreplem1  45161  iccpartigtl  47611