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 1570   ≠ 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  4474  raaanv  4475  iinrab2  5028  iinvdif  5040  riinrab  5044  reusv2lem2  5364  iunopeqop  5498  po2ne  5579  xpriindi  5816  dmxpid  5914  dmxpss  6164  rnxpid  6166  cnvpo  6285  xpcoid  6288  dfpo2  6294  fnprb  7208  fntpb  7209  xpexr  7916  frxp  8125  suppimacnv  8173  fodomr  9127  fodomfir  9298  wdompwdom  9551  en3lp  9594  inf3lemd  9607  prdom2  10010  iunfictbso  10118  infpssrlem4  10309  1re  11233  dedekindle  11399  00id  11410  nn0lt2  12685  nn01to3  12991  ioorebas  13505  fzfi  14037  ssnn0fi  14050  hash2prde  14536  repswsymballbi  14852  cshw0  14866  cshwmodn  14867  cshwsublen  14868  cshwn  14869  cshwlen  14871  cshwidx0  14878  dmtrclfv  15092  cncongr2  16759  cshwsidrepswmod0  17187  cshwshashlem1  17188  cshwshashlem2  17189  cshwsdisj  17191  cntzssv  19456  psgnunilem4  19625  nrhmzr  20700  sdrgacs  20968  mulmarep1gsum2  22797  plyssc  26426  cxpsqrtth  26968  addsqnreup  27680  2sqreultlem  27684  2sqreunnltlem  27687  noresle  27934  oncutlt  28530  n0fincut  28621  axsegcon  29385  axpaschlem  29398  axlowdimlem16  29415  axcontlem7  29428  axcontlem8  29429  axcontlem12  29433  umgrislfupgrlem  29580  edglnl  29601  uhgr2edg  29669  1egrvtxdg0  29972  dfpth2  30194  uspgrn2crct  30277  2pthon3v  30412  clwwlknon0  30564  1pthon2v  30634  1to3vfriswmgr  30761  frgrnbnb  30774  numclwwlk5  30869  siii  31335  h1de2ctlem  32037  riesz3i  32544  unierri  32586  dya2iocuni  34795  sibf0  34846  bnj1143  35300  bnj571  35416  bnj594  35422  bnj852  35431  cgrextend  36589  ifscgr  36625  idinside  36665  btwnconn1lem12  36679  btwnconn1  36682  linethru  36734  bj-xpnzex  37704  ovoliunnfl  38412  voliunnfl  38414  volsupnfl  38415  sn-1ne2  43147  cantnfresb  44166  ax6e2ndeq  45383  lighneal  48515  dfclnbgr6  48773  dfsclnbgr6  48775  gpg5nbgrvtx03starlem1  48985  gpg5nbgrvtx03starlem2  48986  gpg5nbgrvtx03starlem3  48987  gpg5nbgrvtx13starlem1  48988  gpg5nbgrvtx13starlem2  48989  gpg5nbgrvtx13starlem3  48990  gpg5edgnedg  49047  zlmodzxznm  49428  itsclc0yqe  49692  reldmlan2  50544  reldmran2  50545  rellan  50550  relran  50551