Theorem pm2.61ine 3016

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 2937	. . 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 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  pm2.61ne  3018  pm2.61dne  3019  pm2.61iine  3023  raaan  4473  raaanv  4474  iinrab2  5027  iinvdif  5037  riinrab  5041  reusv2lem2  5346  po2ne  5556  xpriindi  5793  dmxpid  5887  dmxpss  6137  rnxpid  6139  cnvpo  6253  xpcoid  6256  dfpo2  6262  fnprb  7164  fntpb  7165  xpexr  7870  frxp  8078  suppimacnv  8126  fodomr  9068  fodomfir  9240  wdompwdom  9495  en3lp  9535  inf3lemd  9548  prdom2  9928  iunfictbso  10036  infpssrlem4  10228  1re  11144  dedekindle  11309  00id  11320  nn0lt2  12567  nn01to3  12866  ioorebas  13379  fzfi  13907  ssnn0fi  13920  hash2prde  14405  repswsymballbi  14715  cshw0  14729  cshwmodn  14730  cshwsublen  14731  cshwn  14732  cshwlen  14734  cshwidx0  14741  dmtrclfv  14953  cncongr2  16607  cshwsidrepswmod0  17034  cshwshashlem1  17035  cshwshashlem2  17036  cshwsdisj  17038  cntzssv  19269  psgnunilem4  19438  nrhmzr  20482  sdrgacs  20746  mulmarep1gsum2  22530  plyssc  26173  cxpsqrtth  26707  addsqnreup  27422  2sqreultlem  27426  2sqreunnltlem  27429  noresle  27677  oncutlt  28272  n0fincut  28363  axsegcon  29012  axpaschlem  29025  axlowdimlem16  29042  axcontlem7  29055  axcontlem8  29056  axcontlem12  29060  umgrislfupgrlem  29207  edglnl  29228  uhgr2edg  29293  1egrvtxdg0  29597  dfpth2  29814  uspgrn2crct  29893  2pthon3v  30028  clwwlknon0  30180  1pthon2v  30240  1to3vfriswmgr  30367  frgrnbnb  30380  numclwwlk5  30475  siii  30941  h1de2ctlem  31643  riesz3i  32150  unierri  32192  dya2iocuni  34461  sibf0  34512  bnj1143  34966  bnj571  35082  bnj594  35088  bnj852  35097  cgrextend  36224  ifscgr  36260  idinside  36300  btwnconn1lem12  36314  btwnconn1  36317  linethru  36369  bj-xpnzex  37207  ovoliunnfl  37913  voliunnfl  37915  volsupnfl  37916  sn-1ne2  42635  cantnfresb  43681  ax6e2ndeq  44915  lighneal  47971  dfclnbgr6  48216  dfsclnbgr6  48218  gpg5nbgrvtx03starlem1  48428  gpg5nbgrvtx03starlem2  48429  gpg5nbgrvtx03starlem3  48430  gpg5nbgrvtx13starlem1  48431  gpg5nbgrvtx13starlem2  48432  gpg5nbgrvtx13starlem3  48433  gpg5edgnedg  48490  zlmodzxznm  48857  itsclc0yqe  49121  reldmlan2  49976  reldmran2  49977  rellan  49982  relran  49983