Theorem pm2.61ine 3009

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2926

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 207  df-ne 2927

This theorem is referenced by:  pm2.61ne  3011  pm2.61dne  3012  pm2.61iine  3016  raaan  4483  raaanv  4484  iinrab2  5037  iinvdif  5047  riinrab  5051  reusv2lem2  5357  po2ne  5565  xpriindi  5803  dmxpid  5897  dmxpss  6147  rnxpid  6149  cnvpo  6263  xpcoid  6266  dfpo2  6272  fnprb  7185  fntpb  7186  xpexr  7897  frxp  8108  suppimacnv  8156  fodomr  9098  fodomfir  9286  wdompwdom  9538  en3lp  9574  inf3lemd  9587  prdom2  9966  iunfictbso  10074  infpssrlem4  10266  1re  11181  dedekindle  11345  00id  11356  nn0lt2  12604  nn01to3  12907  ioorebas  13419  fzfi  13944  ssnn0fi  13957  hash2prde  14442  repswsymballbi  14752  cshw0  14766  cshwmodn  14767  cshwsublen  14768  cshwn  14769  cshwlen  14771  cshwidx0  14778  dmtrclfv  14991  cncongr2  16645  cshwsidrepswmod0  17072  cshwshashlem1  17073  cshwshashlem2  17074  cshwsdisj  17076  cntzssv  19267  psgnunilem4  19434  nrhmzr  20453  sdrgacs  20717  mulmarep1gsum2  22468  plyssc  26112  cxpsqrtth  26646  addsqnreup  27361  2sqreultlem  27365  2sqreunnltlem  27368  noresle  27616  onscutlt  28172  n0sfincut  28253  axsegcon  28861  axpaschlem  28874  axlowdimlem16  28891  axcontlem7  28904  axcontlem8  28905  axcontlem12  28909  umgrislfupgrlem  29056  edglnl  29077  uhgr2edg  29142  1egrvtxdg0  29446  dfpth2  29666  uspgrn2crct  29745  2pthon3v  29880  clwwlknon0  30029  1pthon2v  30089  1to3vfriswmgr  30216  frgrnbnb  30229  numclwwlk5  30324  siii  30789  h1de2ctlem  31491  riesz3i  31998  unierri  32040  dya2iocuni  34281  sibf0  34332  bnj1143  34787  bnj571  34903  bnj594  34909  bnj852  34918  cgrextend  36003  ifscgr  36039  idinside  36079  btwnconn1lem12  36093  btwnconn1  36096  linethru  36148  bj-xpnzex  36954  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  sn-1ne2  42260  cantnfresb  43320  ax6e2ndeq  44556  lighneal  47616  dfclnbgr6  47860  dfsclnbgr6  47862  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem2  48067  gpg5nbgrvtx13starlem3  48068  zlmodzxznm  48490  itsclc0yqe  48754  reldmlan2  49610  reldmran2  49611  rellan  49616  relran  49617