Theorem pm2.61ine 3015

Description: Inference eliminating an inequality in an antecedent. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
pm2.61ine.1	⊢ (𝐴 = 𝐵 → 𝜑)
pm2.61ine.2	⊢ (𝐴 ≠ 𝐵 → 𝜑)

Assertion

Ref	Expression
pm2.61ine	⊢ 𝜑

Proof of Theorem pm2.61ine

Step	Hyp	Ref	Expression
1		pm2.61ine.2	. 2 ⊢ (𝐴 ≠ 𝐵 → 𝜑)
2		nne 2936	. . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)
3		pm2.61ine.1	. . 3 ⊢ (𝐴 = 𝐵 → 𝜑)
4	2, 3	sylbi 217	. 2 ⊢ (¬ 𝐴 ≠ 𝐵 → 𝜑)
5	1, 4	pm2.61i 182	1 ⊢ 𝜑

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ 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.61ne  3017  pm2.61dne  3018  pm2.61iine  3022  raaan  4458  raaanv  4459  iinrab2  5012  iinvdif  5022  riinrab  5026  reusv2lem2  5341  iunopeqop  5475  po2ne  5555  xpriindi  5791  dmxpid  5885  dmxpss  6135  rnxpid  6137  cnvpo  6251  xpcoid  6254  dfpo2  6260  fnprb  7163  fntpb  7164  xpexr  7869  frxp  8076  suppimacnv  8124  fodomr  9066  fodomfir  9238  wdompwdom  9493  en3lp  9535  inf3lemd  9548  prdom2  9928  iunfictbso  10036  infpssrlem4  10228  1re  11144  dedekindle  11310  00id  11321  nn0lt2  12592  nn01to3  12891  ioorebas  13404  fzfi  13934  ssnn0fi  13947  hash2prde  14432  repswsymballbi  14742  cshw0  14756  cshwmodn  14757  cshwsublen  14758  cshwn  14759  cshwlen  14761  cshwidx0  14768  dmtrclfv  14980  cncongr2  16637  cshwsidrepswmod0  17065  cshwshashlem1  17066  cshwshashlem2  17067  cshwsdisj  17069  cntzssv  19303  psgnunilem4  19472  nrhmzr  20514  sdrgacs  20778  mulmarep1gsum2  22539  plyssc  26165  cxpsqrtth  26694  addsqnreup  27406  2sqreultlem  27410  2sqreunnltlem  27413  noresle  27661  oncutlt  28256  n0fincut  28347  axsegcon  28996  axpaschlem  29009  axlowdimlem16  29026  axcontlem7  29039  axcontlem8  29040  axcontlem12  29044  umgrislfupgrlem  29191  edglnl  29212  uhgr2edg  29277  1egrvtxdg0  29580  dfpth2  29797  uspgrn2crct  29876  2pthon3v  30011  clwwlknon0  30163  1pthon2v  30223  1to3vfriswmgr  30350  frgrnbnb  30363  numclwwlk5  30458  siii  30924  h1de2ctlem  31626  riesz3i  32133  unierri  32175  dya2iocuni  34427  sibf0  34478  bnj1143  34932  bnj571  35048  bnj594  35054  bnj852  35063  cgrextend  36190  ifscgr  36226  idinside  36266  btwnconn1lem12  36280  btwnconn1  36283  linethru  36335  bj-xpnzex  37266  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  sn-1ne2  42703  cantnfresb  43752  ax6e2ndeq  44986  lighneal  48074  dfclnbgr6  48332  dfsclnbgr6  48334  gpg5nbgrvtx03starlem1  48544  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx03starlem3  48546  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem2  48548  gpg5nbgrvtx13starlem3  48549  gpg5edgnedg  48606  zlmodzxznm  48973  itsclc0yqe  49237  reldmlan2  50092  reldmran2  50093  rellan  50098  relran  50099