Theorem pm2.61dne 3046

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

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

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 2961

This theorem is used by:  pm2.61dane  3047  wefrc  5657  wereu2  5660  frpomin  6345  oe0lem  8504  fisupg  9255  marypha1lem  9400  fiinfg  9468  wdomtr  9544  unxpwdom2  9557  frmin  9728  fpwwe2lem12  10642  grur1a  10819  grutsk  10822  fimaxre2  12175  xlesubadd  13305  cshwidxmod  14864  sqreu  15436  pcxnn0cl  16942  pcxcl  16943  pcmpt  16974  symggen  19584  isabvd  20965  lspprat  21327  mdetralt  22815  ordtrest2lem  23410  ordthauslem  23590  comppfsc  23740  fbssint  24046  fclscf  24233  tgptsmscld  24359  ovoliunnul  25717  itg11  25901  i1fadd  25905  fta1g  26378  plydiveu  26510  fta1  26520  mulcxp  26901  cxpsqrt  26919  ostth3  27853  madebdaylemlrcut  28143  brbtwn2  29310  colinearalg  29315  clwwisshclwws  30433  ordtrest2NEWlem  34376  fissorduni  35538  subfacp1lem5  35713  btwnexch2  36552  fnemeet2  36935  fnejoin2  36937  limsucncmpi  37013  areacirc  38421  sstotbnd2  38483  ssbnd  38497  prdsbnd2  38504  rrncmslem  38541  atnlt  40145  atlelt  40270  llnnlt  40355  lplnnlt  40397  lvolnltN  40450  pmapglb2N  40603  pmapglb2xN  40604  paddasslem14  40665  cdleme27a  41199  sdomne0  44197  sdomne0d  44198  modelaxreplem1  45745  iccpartigtl  48230