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 1569   ≠ 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  5645  wereu2  5648  frpomin  6346  oe0lem  8528  fisupg  9286  fissorduni  9289  marypha1lem  9432  fiinfg  9500  wdomtr  9576  unxpwdom2  9589  frmin  9760  fpwwe2lem12  10734  grur1a  10911  grutsk  10914  fimaxre2  12269  xlesubadd  13400  cshwidxmod  14962  sqreu  15537  pcxnn0cl  17047  pcxcl  17048  pcmpt  17079  symggen  19693  isabvd  21078  lspprat  21440  mdetralt  22932  ordtrest2lem  23530  ordthauslem  23710  comppfsc  23860  fbssint  24166  fclscf  24353  tgptsmscld  24479  ovoliunnul  25837  itg11  26021  i1fadd  26025  fta1g  26497  plydiveu  26628  fta1  26638  mulcxp  27022  cxpsqrt  27040  ostth3  27974  madebdaylemlrcut  28294  brbtwn2  29492  colinearalg  29497  clwwisshclwws  30615  ordtrest2NEWlem  34604  subfacp1lem5  36039  btwnexch2  36884  fnemeet2  37251  fnejoin2  37253  limsucncmpi  37329  areacirc  38740  sstotbnd2  38817  ssbnd  38831  prdsbnd2  38838  rrncmslem  38875  atnlt  40479  atlelt  40604  llnnlt  40689  lplnnlt  40731  lvolnltN  40784  pmapglb2N  40937  pmapglb2xN  40938  paddasslem14  40999  cdleme27a  41533  sdomne0  44523  sdomne0d  44524  modelaxreplem1  46076  iccpartigtl  48613