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  19242  psgnunilem4  19411  nrhmzr  20457  sdrgacs  20721  mulmarep1gsum2  22494  plyssc  26138  cxpsqrtth  26672  addsqnreup  27387  2sqreultlem  27391  2sqreunnltlem  27394  noresle  27642  onscutlt  28205  n0sfincut  28286  axsegcon  28907  axpaschlem  28920  axlowdimlem16  28937  axcontlem7  28950  axcontlem8  28951  axcontlem12  28955  umgrislfupgrlem  29102  edglnl  29123  uhgr2edg  29188  1egrvtxdg0  29492  dfpth2  29709  uspgrn2crct  29788  2pthon3v  29923  clwwlknon0  30072  1pthon2v  30132  1to3vfriswmgr  30259  frgrnbnb  30272  numclwwlk5  30367  siii  30832  h1de2ctlem  31534  riesz3i  32041  unierri  32083  dya2iocuni  34267  sibf0  34318  bnj1143  34773  bnj571  34889  bnj594  34895  bnj852  34904  cgrextend  35989  ifscgr  36025  idinside  36065  btwnconn1lem12  36079  btwnconn1  36082  linethru  36134  bj-xpnzex  36940  ovoliunnfl  37649  voliunnfl  37651  volsupnfl  37652  sn-1ne2  42246  cantnfresb  43306  ax6e2ndeq  44542  lighneal  47605  dfclnbgr6  47849  dfsclnbgr6  47851  gpg5nbgrvtx03starlem1  48052  gpg5nbgrvtx03starlem2  48053  gpg5nbgrvtx03starlem3  48054  gpg5nbgrvtx13starlem1  48055  gpg5nbgrvtx13starlem2  48056  gpg5nbgrvtx13starlem3  48057  zlmodzxznm  48479  itsclc0yqe  48743  reldmlan2  49599  reldmran2  49600  rellan  49605  relran  49606