Theorem pm2.61ine 3008

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 2929	. . 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 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  pm2.61ne  3010  pm2.61dne  3011  pm2.61iine  3015  raaan  4480  raaanv  4481  iinrab2  5034  iinvdif  5044  riinrab  5048  reusv2lem2  5354  po2ne  5562  xpriindi  5800  dmxpid  5894  dmxpss  6144  rnxpid  6146  cnvpo  6260  xpcoid  6263  dfpo2  6269  fnprb  7182  fntpb  7183  xpexr  7894  frxp  8105  suppimacnv  8153  fodomr  9092  fodomfir  9279  wdompwdom  9531  en3lp  9567  inf3lemd  9580  prdom2  9959  iunfictbso  10067  infpssrlem4  10259  1re  11174  dedekindle  11338  00id  11349  nn0lt2  12597  nn01to3  12900  ioorebas  13412  fzfi  13937  ssnn0fi  13950  hash2prde  14435  repswsymballbi  14745  cshw0  14759  cshwmodn  14760  cshwsublen  14761  cshwn  14762  cshwlen  14764  cshwidx0  14771  dmtrclfv  14984  cncongr2  16638  cshwsidrepswmod0  17065  cshwshashlem1  17066  cshwshashlem2  17067  cshwsdisj  17069  cntzssv  19260  psgnunilem4  19427  nrhmzr  20446  sdrgacs  20710  mulmarep1gsum2  22461  plyssc  26105  cxpsqrtth  26639  addsqnreup  27354  2sqreultlem  27358  2sqreunnltlem  27361  noresle  27609  onscutlt  28165  n0sfincut  28246  axsegcon  28854  axpaschlem  28867  axlowdimlem16  28884  axcontlem7  28897  axcontlem8  28898  axcontlem12  28902  umgrislfupgrlem  29049  edglnl  29070  uhgr2edg  29135  1egrvtxdg0  29439  dfpth2  29659  uspgrn2crct  29738  2pthon3v  29873  clwwlknon0  30022  1pthon2v  30082  1to3vfriswmgr  30209  frgrnbnb  30222  numclwwlk5  30317  siii  30782  h1de2ctlem  31484  riesz3i  31991  unierri  32033  dya2iocuni  34274  sibf0  34325  bnj1143  34780  bnj571  34896  bnj594  34902  bnj852  34911  cgrextend  35996  ifscgr  36032  idinside  36072  btwnconn1lem12  36086  btwnconn1  36089  linethru  36141  bj-xpnzex  36947  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  sn-1ne2  42253  cantnfresb  43313  ax6e2ndeq  44549  lighneal  47612  dfclnbgr6  47856  dfsclnbgr6  47858  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem2  48063  gpg5nbgrvtx13starlem3  48064  zlmodzxznm  48486  itsclc0yqe  48750  reldmlan2  49606  reldmran2  49607  rellan  49612  relran  49613