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  4468  raaanv  4469  iinrab2  5019  iinvdif  5029  riinrab  5033  reusv2lem2  5338  po2ne  5543  xpriindi  5779  dmxpid  5872  dmxpss  6120  rnxpid  6122  cnvpo  6235  xpcoid  6238  dfpo2  6244  fnprb  7144  fntpb  7145  xpexr  7851  frxp  8059  suppimacnv  8107  fodomr  9045  fodomfir  9218  wdompwdom  9470  en3lp  9510  inf3lemd  9523  prdom2  9900  iunfictbso  10008  infpssrlem4  10200  1re  11115  dedekindle  11280  00id  11291  nn0lt2  12539  nn01to3  12842  ioorebas  13354  fzfi  13879  ssnn0fi  13892  hash2prde  14377  repswsymballbi  14686  cshw0  14700  cshwmodn  14701  cshwsublen  14702  cshwn  14703  cshwlen  14705  cshwidx0  14712  dmtrclfv  14925  cncongr2  16579  cshwsidrepswmod0  17006  cshwshashlem1  17007  cshwshashlem2  17008  cshwsdisj  17010  cntzssv  19207  psgnunilem4  19376  nrhmzr  20422  sdrgacs  20686  mulmarep1gsum2  22459  plyssc  26103  cxpsqrtth  26637  addsqnreup  27352  2sqreultlem  27356  2sqreunnltlem  27359  noresle  27607  onscutlt  28170  n0sfincut  28251  axsegcon  28872  axpaschlem  28885  axlowdimlem16  28902  axcontlem7  28915  axcontlem8  28916  axcontlem12  28920  umgrislfupgrlem  29067  edglnl  29088  uhgr2edg  29153  1egrvtxdg0  29457  dfpth2  29674  uspgrn2crct  29753  2pthon3v  29888  clwwlknon0  30037  1pthon2v  30097  1to3vfriswmgr  30224  frgrnbnb  30237  numclwwlk5  30332  siii  30797  h1de2ctlem  31499  riesz3i  32006  unierri  32048  dya2iocuni  34251  sibf0  34302  bnj1143  34757  bnj571  34873  bnj594  34879  bnj852  34888  cgrextend  35982  ifscgr  36018  idinside  36058  btwnconn1lem12  36072  btwnconn1  36075  linethru  36127  bj-xpnzex  36933  ovoliunnfl  37642  voliunnfl  37644  volsupnfl  37645  sn-1ne2  42238  cantnfresb  43297  ax6e2ndeq  44533  lighneal  47595  dfclnbgr6  47840  dfsclnbgr6  47842  gpg5nbgrvtx03starlem1  48052  gpg5nbgrvtx03starlem2  48053  gpg5nbgrvtx03starlem3  48054  gpg5nbgrvtx13starlem1  48055  gpg5nbgrvtx13starlem2  48056  gpg5nbgrvtx13starlem3  48057  gpg5edgnedg  48114  zlmodzxznm  48482  itsclc0yqe  48746  reldmlan2  49602  reldmran2  49603  rellan  49608  relran  49609