Theorem pm2.61ine 3027

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2942

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 206  df-ne 2943

This theorem is referenced by:  pm2.61ne  3029  pm2.61dne  3030  pm2.61iine  3034  raaan  4448  raaanv  4449  iinrab2  4995  iinvdif  5005  riinrab  5009  reusv2lem2  5317  po2ne  5510  xpriindi  5734  dmxpid  5828  dmxpss  6063  rnxpid  6065  cnvpo  6179  xpcoid  6182  dfpo2  6188  fnprb  7066  fntpb  7067  xpexr  7739  frxp  7938  suppimacnv  7961  fodomr  8864  wdompwdom  9267  en3lp  9302  inf3lemd  9315  prdom2  9693  iunfictbso  9801  infpssrlem4  9993  1re  10906  dedekindle  11069  00id  11080  nn0lt2  12313  nn01to3  12610  ioorebas  13112  fzfi  13620  ssnn0fi  13633  hash2prde  14112  repswsymballbi  14421  cshw0  14435  cshwmodn  14436  cshwsublen  14437  cshwn  14438  cshwlen  14440  cshwidx0  14447  dmtrclfv  14657  cncongr2  16301  cshwsidrepswmod0  16724  cshwshashlem1  16725  cshwshashlem2  16726  cshwsdisj  16728  cntzssv  18849  psgnunilem4  19020  sdrgacs  19984  mulmarep1gsum2  21631  plyssc  25266  cxpsqrtth  25789  addsqnreup  26496  2sqreultlem  26500  2sqreunnltlem  26503  axsegcon  27198  axpaschlem  27211  axlowdimlem16  27228  axcontlem7  27241  axcontlem8  27242  axcontlem12  27246  umgrislfupgrlem  27395  edglnl  27416  uhgr2edg  27478  1egrvtxdg0  27781  uspgrn2crct  28074  2pthon3v  28209  clwwlknon0  28358  1pthon2v  28418  1to3vfriswmgr  28545  frgrnbnb  28558  numclwwlk5  28653  siii  29116  h1de2ctlem  29818  riesz3i  30325  unierri  30367  dya2iocuni  32150  sibf0  32201  bnj1143  32670  bnj571  32786  bnj594  32792  bnj852  32801  noresle  33827  cgrextend  34237  ifscgr  34273  idinside  34313  btwnconn1lem12  34327  btwnconn1  34330  linethru  34382  bj-xpnzex  35076  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  sn-1ne2  40216  ax6e2ndeq  42068  lighneal  44951  nrhmzr  45319  zlmodzxznm  45726  itsclc0yqe  45995