Theorem pm2.61ine 3042

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2959

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2960

This theorem is used by:  pm2.61ne  3044  pm2.61dne  3045  pm2.61iine  3049  raaan  4477  raaanv  4478  iinrab2  5033  iinvdif  5045  riinrab  5049  reusv2lem2  5368  iunopeqop  5501  po2ne  5582  xpriindi  5823  dmxpid  5924  dmxpss  6181  rnxpid  6183  cnvpo  6314  xpcoid  6319  dfpo2  6325  fnprb  7245  fntpb  7246  xpexr  7964  frxp  8175  suppimacnv  8229  fodomr  9185  fodomfir  9357  wdompwdom  9609  en3lp  9652  inf3lemd  9665  prdom2  10124  iunfictbso  10232  infpssrlem4  10423  1re  11347  dedekindle  11513  00id  11524  nn0lt2  12802  nn01to3  13108  ioorebas  13622  fzfi  14155  ssnn0fi  14168  hash2prde  14656  repswsymballbi  14973  cshw0  14987  cshwmodn  14988  cshwsublen  14989  cshwn  14990  cshwlen  14992  cshwidx0  14999  dmtrclfv  15214  cncongr2  16887  cshwsidrepswmod0  17316  cshwshashlem1  17317  cshwshashlem2  17318  cshwsdisj  17320  cntzssv  19593  psgnunilem4  19762  nrhmzr  20840  sdrgacs  21109  mulmarep1gsum2  22944  plyssc  26573  cxpsqrtth  27115  addsqnreup  27827  2sqreultlem  27831  2sqreunnltlem  27834  noresle  28111  oncutlt  28707  n0fincut  28798  axsegcon  29562  axpaschlem  29575  axlowdimlem16  29592  axcontlem7  29605  axcontlem8  29606  axcontlem12  29610  umgrislfupgrlem  29757  edglnl  29778  uhgr2edg  29846  1egrvtxdg0  30149  dfpth2  30371  uspgrn2crct  30454  2pthon3v  30589  clwwlknon0  30741  1pthon2v  30811  1to3vfriswmgr  30938  frgrnbnb  30951  numclwwlk5  31046  siii  31512  h1de2ctlem  32214  riesz3i  32721  unierri  32763  dya2iocuni  35026  sibf0  35077  bnj1143  35531  bnj571  35647  bnj594  35653  bnj852  35662  cgrextend  36988  ifscgr  37024  idinside  37064  btwnconn1lem12  37078  btwnconn1  37081  linethru  37133  bj-xpnzex  38087  ovoliunnfl  38848  voliunnfl  38850  volsupnfl  38851  sn-1ne2  43596  cantnfresb  44587  ax6e2ndeq  45802  lighneal  48969  dfclnbgr6  49227  dfsclnbgr6  49229  gpg5nbgrvtx03starlem1  49439  gpg5nbgrvtx03starlem2  49440  gpg5nbgrvtx03starlem3  49441  gpg5nbgrvtx13starlem1  49442  gpg5nbgrvtx13starlem2  49443  gpg5nbgrvtx13starlem3  49444  gpg5edgnedg  49501  zlmodzxznm  49940  itsclc0yqe  50204  reldmlan2  51131  reldmran2  51132  rellan  51137  relran  51138