Theorem pm2.61ine 3070

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ≠ wne 2987

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 2988

This theorem is referenced by:  pm2.61ne  3072  pm2.61iine  3077  raaan  4418  raaanv  4419  iinrab2  4955  iinvdif  4965  riinrab  4969  reusv2lem2  5265  po2ne  5453  xpriindi  5671  dmxpid  5764  dmxpss  5995  rnxpid  5997  cnvpo  6106  xpcoid  6109  fnprb  6948  fntpb  6949  xpexr  7605  frxp  7803  suppimacnv  7824  fodomr  8652  wdompwdom  9026  en3lp  9061  inf3lemd  9074  prdom2  9417  iunfictbso  9525  infpssrlem4  9717  1re  10630  dedekindle  10793  00id  10804  nn0lt2  12033  nn01to3  12329  ioorebas  12829  fzfi  13335  ssnn0fi  13348  hash2prde  13824  repswsymballbi  14133  cshw0  14147  cshwmodn  14148  cshwsublen  14149  cshwn  14150  cshwlen  14152  cshwidx0  14159  dmtrclfv  14369  cncongr2  16002  cshwsidrepswmod0  16420  cshwshashlem1  16421  cshwshashlem2  16422  cshwsdisj  16424  cntzssv  18450  psgnunilem4  18617  sdrgacs  19573  mulmarep1gsum2  21179  plyssc  24797  cxpsqrtth  25320  addsqnreup  26027  2sqreultlem  26031  2sqreunnltlem  26034  axsegcon  26721  axpaschlem  26734  axlowdimlem16  26751  axcontlem7  26764  axcontlem8  26765  axcontlem12  26769  umgrislfupgrlem  26915  edglnl  26936  uhgr2edg  26998  1egrvtxdg0  27301  uspgrn2crct  27594  2pthon3v  27729  clwwlknon0  27878  1pthon2v  27938  1to3vfriswmgr  28065  frgrnbnb  28078  numclwwlk5  28173  siii  28636  h1de2ctlem  29338  riesz3i  29845  unierri  29887  dya2iocuni  31651  sibf0  31702  bnj1143  32172  bnj571  32288  bnj594  32294  bnj852  32303  dfpo2  33104  noresle  33313  cgrextend  33582  ifscgr  33618  idinside  33658  btwnconn1lem12  33672  btwnconn1  33675  linethru  33727  bj-xpnzex  34395  ovoliunnfl  35099  voliunnfl  35101  volsupnfl  35102  sn-1ne2  39466  ax6e2ndeq  41265  lighneal  44129  nrhmzr  44497  zlmodzxznm  44906  itsclc0yqe  45175