Theorem pm2.61dne 3050

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 33	. 2 ⊢ (𝐴 = 𝐵 → (𝜑 → 𝜓))
3		pm2.61dne.2	. . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))
4	3	com12 33	. 2 ⊢ (𝐴 ≠ 𝐵 → (𝜑 → 𝜓))
5	2, 4	pm2.61ine 3047	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   = wceq 1567   ≠ wne 2964

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 210  df-ne 2965

This theorem is referenced by:  pm2.61dane  3051  wefrc  5656  wereu2  5659  frpomin  6342  oe0lem  8497  fisupg  9247  marypha1lem  9392  fiinfg  9460  wdomtr  9536  unxpwdom2  9549  frmin  9720  fpwwe2lem12  10626  grur1a  10803  grutsk  10806  fimaxre2  12159  xlesubadd  13288  cshwidxmod  14839  sqreu  15411  pcxnn0cl  16919  pcxcl  16920  pcmpt  16951  symggen  19539  isabvd  20892  lspprat  21254  mdetralt  22733  ordtrest2lem  23328  ordthauslem  23508  comppfsc  23657  fbssint  23963  fclscf  24150  tgptsmscld  24276  ovoliunnul  25634  itg11  25818  i1fadd  25822  fta1g  26295  plydiveu  26427  fta1  26437  mulcxp  26815  cxpsqrt  26833  ostth3  27767  madebdaylemlrcut  28057  brbtwn2  29195  colinearalg  29200  clwwisshclwws  30306  ordtrest2NEWlem  34256  fissorduni  35422  subfacp1lem5  35574  btwnexch2  36413  fnemeet2  36766  fnejoin2  36768  limsucncmpi  36844  areacirc  38251  sstotbnd2  38312  ssbnd  38326  prdsbnd2  38333  rrncmslem  38370  atnlt  39976  atlelt  40101  llnnlt  40186  lplnnlt  40228  lvolnltN  40281  pmapglb2N  40434  pmapglb2xN  40435  paddasslem14  40496  cdleme27a  41030  sdomne0  44030  sdomne0d  44031  modelaxreplem1  45578  iccpartigtl  48060