Theorem pm2.61ine 3047

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1567   ≠ wne 2964

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 210  df-ne 2965

This theorem is referenced by:  pm2.61ne  3049  pm2.61dne  3050  pm2.61iine  3054  raaan  4484  raaanv  4485  iinrab2  5038  iinvdif  5050  riinrab  5054  reusv2lem2  5371  iunopeqop  5505  po2ne  5586  xpriindi  5823  dmxpid  5921  dmxpss  6170  rnxpid  6172  cnvpo  6289  xpcoid  6292  dfpo2  6298  fnprb  7207  fntpb  7208  xpexr  7914  frxp  8121  suppimacnv  8169  fodomr  9115  fodomfir  9286  wdompwdom  9539  en3lp  9582  inf3lemd  9595  prdom2  9989  iunfictbso  10097  infpssrlem4  10289  1re  11207  dedekindle  11373  00id  11384  nn0lt2  12658  nn01to3  12964  ioorebas  13477  fzfi  14007  ssnn0fi  14020  hash2prde  14506  repswsymballbi  14816  cshw0  14830  cshwmodn  14831  cshwsublen  14832  cshwn  14833  cshwlen  14835  cshwidx0  14842  dmtrclfv  15054  cncongr2  16725  cshwsidrepswmod0  17153  cshwshashlem1  17154  cshwshashlem2  17155  cshwsdisj  17157  cntzssv  19397  psgnunilem4  19566  nrhmzr  20621  sdrgacs  20881  mulmarep1gsum2  22699  plyssc  26325  cxpsqrtth  26860  addsqnreup  27572  2sqreultlem  27576  2sqreunnltlem  27579  noresle  27826  oncutlt  28422  n0fincut  28513  axsegcon  29217  axpaschlem  29230  axlowdimlem16  29247  axcontlem7  29260  axcontlem8  29261  axcontlem12  29265  umgrislfupgrlem  29412  edglnl  29433  uhgr2edg  29498  1egrvtxdg0  29801  dfpth2  30018  uspgrn2crct  30097  2pthon3v  30232  clwwlknon0  30384  1pthon2v  30444  1to3vfriswmgr  30571  frgrnbnb  30584  numclwwlk5  30679  siii  31145  h1de2ctlem  31847  riesz3i  32354  unierri  32396  dya2iocuni  34617  sibf0  34668  bnj1143  35122  bnj571  35238  bnj594  35244  bnj852  35253  cgrextend  36398  ifscgr  36434  idinside  36474  btwnconn1lem12  36488  btwnconn1  36491  linethru  36543  bj-xpnzex  37482  ovoliunnfl  38200  voliunnfl  38202  volsupnfl  38203  sn-1ne2  42921  cantnfresb  43942  ax6e2ndeq  45159  lighneal  48251  dfclnbgr6  48509  dfsclnbgr6  48511  gpg5nbgrvtx03starlem1  48721  gpg5nbgrvtx03starlem2  48722  gpg5nbgrvtx03starlem3  48723  gpg5nbgrvtx13starlem1  48724  gpg5nbgrvtx13starlem2  48725  gpg5nbgrvtx13starlem3  48726  gpg5edgnedg  48783  zlmodzxznm  49161  itsclc0yqe  49425  reldmlan2  50279  reldmran2  50280  rellan  50285  relran  50286