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  4476  raaanv  4477  iinrab2  5029  iinvdif  5039  riinrab  5043  reusv2lem2  5349  po2ne  5555  xpriindi  5790  dmxpid  5883  dmxpss  6132  rnxpid  6134  cnvpo  6248  xpcoid  6251  dfpo2  6257  fnprb  7164  fntpb  7165  xpexr  7874  frxp  8082  suppimacnv  8130  fodomr  9069  fodomfir  9255  wdompwdom  9507  en3lp  9543  inf3lemd  9556  prdom2  9935  iunfictbso  10043  infpssrlem4  10235  1re  11150  dedekindle  11314  00id  11325  nn0lt2  12573  nn01to3  12876  ioorebas  13388  fzfi  13913  ssnn0fi  13926  hash2prde  14411  repswsymballbi  14721  cshw0  14735  cshwmodn  14736  cshwsublen  14737  cshwn  14738  cshwlen  14740  cshwidx0  14747  dmtrclfv  14960  cncongr2  16614  cshwsidrepswmod0  17041  cshwshashlem1  17042  cshwshashlem2  17043  cshwsdisj  17045  cntzssv  19236  psgnunilem4  19403  nrhmzr  20422  sdrgacs  20686  mulmarep1gsum2  22437  plyssc  26081  cxpsqrtth  26615  addsqnreup  27330  2sqreultlem  27334  2sqreunnltlem  27337  noresle  27585  onscutlt  28141  n0sfincut  28222  axsegcon  28830  axpaschlem  28843  axlowdimlem16  28860  axcontlem7  28873  axcontlem8  28874  axcontlem12  28878  umgrislfupgrlem  29025  edglnl  29046  uhgr2edg  29111  1egrvtxdg0  29415  dfpth2  29632  uspgrn2crct  29711  2pthon3v  29846  clwwlknon0  29995  1pthon2v  30055  1to3vfriswmgr  30182  frgrnbnb  30195  numclwwlk5  30290  siii  30755  h1de2ctlem  31457  riesz3i  31964  unierri  32006  dya2iocuni  34247  sibf0  34298  bnj1143  34753  bnj571  34869  bnj594  34875  bnj852  34884  cgrextend  35969  ifscgr  36005  idinside  36045  btwnconn1lem12  36059  btwnconn1  36062  linethru  36114  bj-xpnzex  36920  ovoliunnfl  37629  voliunnfl  37631  volsupnfl  37632  sn-1ne2  42226  cantnfresb  43286  ax6e2ndeq  44522  lighneal  47585  dfclnbgr6  47829  dfsclnbgr6  47831  gpg5nbgrvtx03starlem1  48032  gpg5nbgrvtx03starlem2  48033  gpg5nbgrvtx03starlem3  48034  gpg5nbgrvtx13starlem1  48035  gpg5nbgrvtx13starlem2  48036  gpg5nbgrvtx13starlem3  48037  zlmodzxznm  48459  itsclc0yqe  48723  reldmlan2  49579  reldmran2  49580  rellan  49585  relran  49586