Theorem pm2.61ine 3015

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1632   ≠ wne 2932

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 197  df-ne 2933

This theorem is referenced by:  pm2.61ne  3017  pm2.61iine  3022  rgenzOLD  4221  raaan  4226  iinrab2  4735  iinvdif  4744  riinrab  4748  reusv2lem2  5018  reusv2lem2OLD  5019  xpriindi  5414  dmxpid  5500  dmxpss  5723  rnxpid  5725  cnvpo  5834  xpcoid  5837  fnprb  6636  fntpb  6637  xpexr  7271  frxp  7455  suppimacnv  7474  fodomr  8276  wdompwdom  8648  en3lp  8682  inf3lemd  8697  prdom2  9019  iunfictbso  9127  infpssrlem4  9320  1re  10231  dedekindle  10393  00id  10403  nn0lt2  11632  nn01to3  11974  ioorebas  12468  fzfi  12965  ssnn0fi  12978  hash2prde  13444  repswsymballbi  13727  cshw0  13740  cshwmodn  13741  cshwsublen  13742  cshwn  13743  cshwlen  13745  cshwidx0  13752  dmtrclfv  13958  cncongr2  15584  cshwsidrepswmod0  16003  cshwshashlem1  16004  cshwshashlem2  16005  cshwsdisj  16007  cntzssv  17961  psgnunilem4  18117  mulmarep1gsum2  20582  plyssc  24155  axsegcon  26006  axpaschlem  26019  axlowdimlem16  26036  axcontlem7  26049  axcontlem8  26050  axcontlem12  26054  umgrislfupgrlem  26216  edglnl  26237  uhgr2edg  26299  1egrvtxdg0  26617  uspgrn2crct  26911  2pthon3v  27063  clwwlknon0  27240  1pthon2v  27305  1to3vfriswmgr  27434  frgrnbnb  27447  numclwwlk5  27556  siii  28017  h1de2ctlem  28723  riesz3i  29230  unierri  29272  dya2iocuni  30654  sibf0  30705  bnj1143  31168  bnj571  31283  bnj594  31289  bnj852  31298  dfpo2  31952  noresle  32152  cgrextend  32421  ifscgr  32457  idinside  32497  btwnconn1lem12  32511  btwnconn1  32514  linethru  32566  bj-xpnzex  33252  ovoliunnfl  33764  voliunnfl  33766  volsupnfl  33767  sdrgacs  38273  ax6e2ndeq  39277  lighneal  42038  nrhmzr  42383  zlmodzxznm  42796