Theorem pm2.61ine 3022

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 2941	. . 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 1536   ≠ wne 2937

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 2938

This theorem is referenced by:  pm2.61ne  3024  pm2.61dne  3025  pm2.61iine  3029  raaan  4522  raaanv  4523  iinrab2  5074  iinvdif  5084  riinrab  5088  reusv2lem2  5404  po2ne  5612  xpriindi  5849  dmxpid  5943  dmxpss  6192  rnxpid  6194  cnvpo  6308  xpcoid  6311  dfpo2  6317  fnprb  7227  fntpb  7228  xpexr  7940  frxp  8149  suppimacnv  8197  fodomr  9166  fodomfir  9365  wdompwdom  9615  en3lp  9651  inf3lemd  9664  prdom2  10043  iunfictbso  10151  infpssrlem4  10343  1re  11258  dedekindle  11422  00id  11433  nn0lt2  12678  nn01to3  12980  ioorebas  13487  fzfi  14009  ssnn0fi  14022  hash2prde  14505  repswsymballbi  14814  cshw0  14828  cshwmodn  14829  cshwsublen  14830  cshwn  14831  cshwlen  14833  cshwidx0  14840  dmtrclfv  15053  cncongr2  16701  cshwsidrepswmod0  17128  cshwshashlem1  17129  cshwshashlem2  17130  cshwsdisj  17132  cntzssv  19358  psgnunilem4  19529  nrhmzr  20553  sdrgacs  20818  mulmarep1gsum2  22595  plyssc  26253  cxpsqrtth  26786  addsqnreup  27501  2sqreultlem  27505  2sqreunnltlem  27508  noresle  27756  axsegcon  28956  axpaschlem  28969  axlowdimlem16  28986  axcontlem7  28999  axcontlem8  29000  axcontlem12  29004  umgrislfupgrlem  29153  edglnl  29174  uhgr2edg  29239  1egrvtxdg0  29543  uspgrn2crct  29837  2pthon3v  29972  clwwlknon0  30121  1pthon2v  30181  1to3vfriswmgr  30308  frgrnbnb  30321  numclwwlk5  30416  siii  30881  h1de2ctlem  31583  riesz3i  32090  unierri  32132  dya2iocuni  34264  sibf0  34315  bnj1143  34782  bnj571  34898  bnj594  34904  bnj852  34913  cgrextend  35989  ifscgr  36025  idinside  36065  btwnconn1lem12  36079  btwnconn1  36082  linethru  36134  bj-xpnzex  36941  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  sn-1ne2  42278  cantnfresb  43313  ax6e2ndeq  44556  lighneal  47535  dfclnbgr6  47779  dfsclnbgr6  47781  gpg5nbgrvtx03starlem1  47958  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx03starlem3  47960  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem2  47962  gpg5nbgrvtx13starlem3  47963  zlmodzxznm  48342  itsclc0yqe  48610