Theorem pm2.61dne 3041

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2956

This theorem is used by:  pm2.61dane  3042  wefrc  5649  wereu2  5652  frpomin  6338  oe0lem  8500  fisupg  9258  marypha1lem  9403  fiinfg  9471  wdomtr  9547  unxpwdom2  9560  frmin  9731  fpwwe2lem12  10651  grur1a  10828  grutsk  10831  fimaxre2  12184  xlesubadd  13315  cshwidxmod  14874  sqreu  15448  pcxnn0cl  16952  pcxcl  16953  pcmpt  16984  symggen  19597  isabvd  20978  lspprat  21340  mdetralt  22830  ordtrest2lem  23428  ordthauslem  23608  comppfsc  23758  fbssint  24064  fclscf  24251  tgptsmscld  24377  ovoliunnul  25735  itg11  25919  i1fadd  25923  fta1g  26395  plydiveu  26528  fta1  26538  mulcxp  26922  cxpsqrt  26940  ostth3  27874  madebdaylemlrcut  28164  brbtwn2  29362  colinearalg  29367  clwwisshclwws  30485  ordtrest2NEWlem  34432  fissorduni  35594  subfacp1lem5  35763  btwnexch2  36603  fnemeet2  36986  fnejoin2  36988  limsucncmpi  37064  areacirc  38462  sstotbnd2  38524  ssbnd  38538  prdsbnd2  38545  rrncmslem  38582  atnlt  40186  atlelt  40311  llnnlt  40396  lplnnlt  40438  lvolnltN  40491  pmapglb2N  40644  pmapglb2xN  40645  paddasslem14  40706  cdleme27a  41240  sdomne0  44253  sdomne0d  44254  modelaxreplem1  45801  iccpartigtl  48323