Theorem pm2.61dne 3011

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

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

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 2926

This theorem is referenced by:  pm2.61dane  3012  wefrc  5625  wereu2  5628  frpomin  6301  oe0lem  8454  fisupg  9211  marypha1lem  9360  fiinfg  9428  wdomtr  9504  unxpwdom2  9517  frmin  9678  fpwwe2lem12  10571  grur1a  10748  grutsk  10751  fimaxre2  12104  xlesubadd  13199  cshwidxmod  14744  sqreu  15303  pcxnn0cl  16807  pcxcl  16808  pcmpt  16839  symggen  19376  isabvd  20697  lspprat  21039  mdetralt  22471  ordtrest2lem  23066  ordthauslem  23246  comppfsc  23395  fbssint  23701  fclscf  23888  tgptsmscld  24014  ovoliunnul  25384  itg11  25568  i1fadd  25572  fta1g  26051  plydiveu  26182  fta1  26192  mulcxp  26570  cxpsqrt  26588  ostth3  27525  madebdaylemlrcut  27786  brbtwn2  28808  colinearalg  28813  clwwisshclwws  29917  ordtrest2NEWlem  33885  subfacp1lem5  35144  btwnexch2  35984  fnemeet2  36328  fnejoin2  36330  limsucncmpi  36406  areacirc  37680  sstotbnd2  37741  ssbnd  37755  prdsbnd2  37762  rrncmslem  37799  atnlt  39279  atlelt  39405  llnnlt  39490  lplnnlt  39532  lvolnltN  39585  pmapglb2N  39738  pmapglb2xN  39739  paddasslem14  39800  cdleme27a  40334  sdomne0  43375  sdomne0d  43376  modelaxreplem1  44941  iccpartigtl  47397