Theorem pm2.61ine 3041

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 2962	. . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)
3		pm2.61ine.1	. . 3 ⊢ (𝐴 = 𝐵 → 𝜑)
4	2, 3	sylbi 220	. 2 ⊢ (¬ 𝐴 ≠ 𝐵 → 𝜑)
5	1, 4	pm2.61i 184	1 ⊢ 𝜑

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2958

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 210  df-ne 2959

This theorem is referenced by:  pm2.61ne  3043  pm2.61dne  3044  pm2.61iine  3048  raaan  4479  raaanv  4480  iinrab2  5034  iinvdif  5046  riinrab  5050  reusv2lem2  5370  iunopeqop  5504  po2ne  5585  xpriindi  5822  dmxpid  5920  dmxpss  6169  rnxpid  6171  cnvpo  6288  xpcoid  6291  dfpo2  6297  fnprb  7206  fntpb  7207  xpexr  7911  frxp  8118  suppimacnv  8166  fodomr  9112  fodomfir  9283  wdompwdom  9536  en3lp  9579  inf3lemd  9592  prdom2  9986  iunfictbso  10094  infpssrlem4  10285  1re  11203  dedekindle  11369  00id  11380  nn0lt2  12654  nn01to3  12960  ioorebas  13473  fzfi  14004  ssnn0fi  14017  hash2prde  14503  repswsymballbi  14813  cshw0  14827  cshwmodn  14828  cshwsublen  14829  cshwn  14830  cshwlen  14832  cshwidx0  14839  dmtrclfv  15051  cncongr2  16721  cshwsidrepswmod0  17149  cshwshashlem1  17150  cshwshashlem2  17151  cshwsdisj  17153  cntzssv  19393  psgnunilem4  19562  nrhmzr  20636  sdrgacs  20904  mulmarep1gsum2  22731  plyssc  26357  cxpsqrtth  26895  addsqnreup  27607  2sqreultlem  27611  2sqreunnltlem  27614  noresle  27861  oncutlt  28457  n0fincut  28548  axsegcon  29277  axpaschlem  29290  axlowdimlem16  29307  axcontlem7  29320  axcontlem8  29321  axcontlem12  29325  umgrislfupgrlem  29472  edglnl  29493  uhgr2edg  29558  1egrvtxdg0  29861  dfpth2  30078  uspgrn2crct  30157  2pthon3v  30292  clwwlknon0  30444  1pthon2v  30504  1to3vfriswmgr  30631  frgrnbnb  30644  numclwwlk5  30739  siii  31205  h1de2ctlem  31907  riesz3i  32414  unierri  32456  dya2iocuni  34673  sibf0  34724  bnj1143  35178  bnj571  35294  bnj594  35300  bnj852  35309  cgrextend  36500  ifscgr  36536  idinside  36576  btwnconn1lem12  36590  btwnconn1  36593  linethru  36645  bj-xpnzex  37595  ovoliunnfl  38313  voliunnfl  38315  volsupnfl  38316  sn-1ne2  43032  cantnfresb  44051  ax6e2ndeq  45268  lighneal  48363  dfclnbgr6  48621  dfsclnbgr6  48623  gpg5nbgrvtx03starlem1  48833  gpg5nbgrvtx03starlem2  48834  gpg5nbgrvtx03starlem3  48835  gpg5nbgrvtx13starlem1  48836  gpg5nbgrvtx13starlem2  48837  gpg5nbgrvtx13starlem3  48838  gpg5edgnedg  48895  zlmodzxznm  49277  itsclc0yqe  49541  reldmlan2  50395  reldmran2  50396  rellan  50401  relran  50402