Theorem pm2.61dne 3018

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

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2932

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 207  df-ne 2933

This theorem is referenced by:  pm2.61dane  3019  wefrc  5618  wereu2  5621  frpomin  6298  oe0lem  8440  fisupg  9188  marypha1lem  9336  fiinfg  9404  wdomtr  9480  unxpwdom2  9493  frmin  9661  fpwwe2lem12  10553  grur1a  10730  grutsk  10733  fimaxre2  12087  xlesubadd  13178  cshwidxmod  14726  sqreu  15284  pcxnn0cl  16788  pcxcl  16789  pcmpt  16820  symggen  19399  isabvd  20745  lspprat  21108  mdetralt  22552  ordtrest2lem  23147  ordthauslem  23327  comppfsc  23476  fbssint  23782  fclscf  23969  tgptsmscld  24095  ovoliunnul  25464  itg11  25648  i1fadd  25652  fta1g  26131  plydiveu  26262  fta1  26272  mulcxp  26650  cxpsqrt  26668  ostth3  27605  madebdaylemlrcut  27895  brbtwn2  28978  colinearalg  28983  clwwisshclwws  30090  ordtrest2NEWlem  34079  fissorduni  35246  subfacp1lem5  35378  btwnexch2  36217  fnemeet2  36561  fnejoin2  36563  limsucncmpi  36639  areacirc  37914  sstotbnd2  37975  ssbnd  37989  prdsbnd2  37996  rrncmslem  38033  atnlt  39573  atlelt  39698  llnnlt  39783  lplnnlt  39825  lvolnltN  39878  pmapglb2N  40031  pmapglb2xN  40032  paddasslem14  40093  cdleme27a  40627  sdomne0  43654  sdomne0d  43655  modelaxreplem1  45219  iccpartigtl  47669