Theorem pm2.61dne 3045

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

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

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 2960

This theorem is used by:  pm2.61dane  3046  wefrc  5652  wereu2  5655  frpomin  6369  oe0lem  8559  fisupg  9317  fissorduni  9320  marypha1lem  9462  fiinfg  9530  wdomtr  9606  unxpwdom2  9619  frmin  9790  fpwwe2lem12  10766  grur1a  10943  grutsk  10946  fimaxre2  12302  xlesubadd  13433  cshwidxmod  14996  sqreu  15572  pcxnn0cl  17082  pcxcl  17083  pcmpt  17114  symggen  19735  isabvd  21120  lspprat  21482  mdetralt  22978  ordtrest2lem  23576  ordthauslem  23756  comppfsc  23906  fbssint  24212  fclscf  24399  tgptsmscld  24525  ovoliunnul  25883  itg11  26067  i1fadd  26071  fta1g  26543  plydiveu  26674  fta1  26684  mulcxp  27070  cxpsqrt  27088  ostth3  28022  madebdaylemlrcut  28342  brbtwn2  29540  colinearalg  29545  clwwisshclwws  30663  ordtrest2NEWlem  34665  subfacp1lem5  36157  btwnexch2  37003  fnemeet2  37370  fnejoin2  37372  limsucncmpi  37448  areacirc  38899  sstotbnd2  38974  ssbnd  38988  prdsbnd2  38995  rrncmslem  39032  atnlt  40636  atlelt  40761  llnnlt  40846  lplnnlt  40888  lvolnltN  40941  pmapglb2N  41094  pmapglb2xN  41095  paddasslem14  41156  cdleme27a  41690  sdomne0  44675  sdomne0d  44676  modelaxreplem1  46232  iccpartigtl  48778