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  5632  wereu2  5635  frpomin  6313  oe0lem  8477  fisupg  9235  marypha1lem  9384  fiinfg  9452  wdomtr  9528  unxpwdom2  9541  frmin  9702  fpwwe2lem12  10595  grur1a  10772  grutsk  10775  fimaxre2  12128  xlesubadd  13223  cshwidxmod  14768  sqreu  15327  pcxnn0cl  16831  pcxcl  16832  pcmpt  16863  symggen  19400  isabvd  20721  lspprat  21063  mdetralt  22495  ordtrest2lem  23090  ordthauslem  23270  comppfsc  23419  fbssint  23725  fclscf  23912  tgptsmscld  24038  ovoliunnul  25408  itg11  25592  i1fadd  25596  fta1g  26075  plydiveu  26206  fta1  26216  mulcxp  26594  cxpsqrt  26612  ostth3  27549  madebdaylemlrcut  27810  brbtwn2  28832  colinearalg  28837  clwwisshclwws  29944  ordtrest2NEWlem  33912  subfacp1lem5  35171  btwnexch2  36011  fnemeet2  36355  fnejoin2  36357  limsucncmpi  36433  areacirc  37707  sstotbnd2  37768  ssbnd  37782  prdsbnd2  37789  rrncmslem  37826  atnlt  39306  atlelt  39432  llnnlt  39517  lplnnlt  39559  lvolnltN  39612  pmapglb2N  39765  pmapglb2xN  39766  paddasslem14  39827  cdleme27a  40361  sdomne0  43402  sdomne0d  43403  modelaxreplem1  44968  iccpartigtl  47424