Theorem pm2.61ine 2877

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 2798	. . 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 1483   ≠ wne 2794

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 2795

This theorem is referenced by:  pm2.61ne  2879  pm2.61iine  2884  rgenzOLD  4077  raaan  4082  iinrab2  4583  iinvdif  4592  riinrab  4596  reusv2lem2  4869  reusv2lem2OLD  4870  xpriindi  5258  dmxpid  5345  dmxpss  5565  rnxpid  5567  cnvpo  5673  xpcoid  5676  fnprb  6472  fntpb  6473  xpexr  7106  frxp  7287  suppimacnv  7306  fodomr  8111  wdompwdom  8483  en3lp  8513  inf3lemd  8524  prdom2  8829  iunfictbso  8937  infpssrlem4  9128  1re  10039  dedekindle  10201  00id  10211  nn0lt2  11440  nn01to3  11781  ioorebas  12275  fzfi  12771  ssnn0fi  12784  hash2prde  13252  repswsymballbi  13527  cshw0  13540  cshwmodn  13541  cshwsublen  13542  cshwn  13543  cshwlen  13545  cshwidx0  13552  dmtrclfv  13759  cncongr2  15382  cshwsidrepswmod0  15801  cshwshashlem1  15802  cshwshashlem2  15803  cshwsdisj  15805  cntzssv  17761  psgnunilem4  17917  mulmarep1gsum2  20380  plyssc  23956  axsegcon  25807  axpaschlem  25820  axlowdimlem16  25837  axcontlem7  25850  axcontlem8  25851  axcontlem12  25855  umgrislfupgrlem  26017  edglnl  26038  uhgr2edg  26100  1egrvtxdg0  26407  uspgrn2crct  26700  2pthon3v  26839  1pthon2v  27013  1to3vfriswmgr  27144  frgrnbnb  27157  numclwwlk5  27246  siii  27708  h1de2ctlem  28414  riesz3i  28921  unierri  28963  dya2iocuni  30345  sibf0  30396  bnj1143  30861  bnj571  30976  bnj594  30982  bnj852  30991  dfpo2  31645  noresle  31846  cgrextend  32115  ifscgr  32151  idinside  32191  btwnconn1lem12  32205  btwnconn1  32208  linethru  32260  bj-xpnzex  32946  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  sdrgacs  37771  ax6e2ndeq  38775  lighneal  41528  nrhmzr  41873  zlmodzxznm  42286