Theorem pm2.61ine 3038

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 2959	. . 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 1569   ≠ wne 2955

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 2956

This theorem is used by:  pm2.61ne  3040  pm2.61dne  3041  pm2.61iine  3045  raaan  4473  raaanv  4474  iinrab2  5027  iinvdif  5039  riinrab  5043  reusv2lem2  5361  iunopeqop  5494  po2ne  5575  xpriindi  5814  dmxpid  5913  dmxpss  6165  rnxpid  6167  cnvpo  6293  xpcoid  6296  dfpo2  6302  fnprb  7218  fntpb  7219  xpexr  7934  frxp  8145  suppimacnv  8199  fodomr  9155  fodomfir  9327  wdompwdom  9579  en3lp  9622  inf3lemd  9635  prdom2  10092  iunfictbso  10200  infpssrlem4  10391  1re  11315  dedekindle  11481  00id  11492  nn0lt2  12769  nn01to3  13075  ioorebas  13589  fzfi  14122  ssnn0fi  14135  hash2prde  14622  repswsymballbi  14939  cshw0  14953  cshwmodn  14954  cshwsublen  14955  cshwn  14956  cshwlen  14958  cshwidx0  14965  dmtrclfv  15180  cncongr2  16852  cshwsidrepswmod0  17281  cshwshashlem1  17282  cshwshashlem2  17283  cshwsdisj  17285  cntzssv  19551  psgnunilem4  19720  nrhmzr  20798  sdrgacs  21067  mulmarep1gsum2  22898  plyssc  26527  cxpsqrtth  27067  addsqnreup  27779  2sqreultlem  27783  2sqreunnltlem  27786  noresle  28063  oncutlt  28659  n0fincut  28750  axsegcon  29514  axpaschlem  29527  axlowdimlem16  29544  axcontlem7  29557  axcontlem8  29558  axcontlem12  29562  umgrislfupgrlem  29709  edglnl  29730  uhgr2edg  29798  1egrvtxdg0  30101  dfpth2  30323  uspgrn2crct  30406  2pthon3v  30541  clwwlknon0  30693  1pthon2v  30763  1to3vfriswmgr  30890  frgrnbnb  30903  numclwwlk5  30998  siii  31464  h1de2ctlem  32166  riesz3i  32673  unierri  32715  dya2iocuni  34965  sibf0  35016  bnj1143  35470  bnj571  35586  bnj594  35592  bnj852  35601  cgrextend  36897  ifscgr  36933  idinside  36973  btwnconn1lem12  36987  btwnconn1  36990  linethru  37042  bj-xpnzex  37996  ovoliunnfl  38717  voliunnfl  38719  volsupnfl  38720  sn-1ne2  43467  cantnfresb  44463  ax6e2ndeq  45678  lighneal  48832  dfclnbgr6  49090  dfsclnbgr6  49092  gpg5nbgrvtx03starlem1  49302  gpg5nbgrvtx03starlem2  49303  gpg5nbgrvtx03starlem3  49304  gpg5nbgrvtx13starlem1  49305  gpg5nbgrvtx13starlem2  49306  gpg5nbgrvtx13starlem3  49307  gpg5edgnedg  49364  zlmodzxznm  49745  itsclc0yqe  50009  reldmlan2  50936  reldmran2  50937  rellan  50942  relran  50943