Theorem pm2.61ine 3029

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2944

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 206  df-ne 2945

This theorem is referenced by:  pm2.61ne  3031  pm2.61dne  3032  pm2.61iine  3036  raaan  4452  raaanv  4453  iinrab2  5000  iinvdif  5010  riinrab  5014  reusv2lem2  5323  po2ne  5520  xpriindi  5748  dmxpid  5842  dmxpss  6079  rnxpid  6081  cnvpo  6194  xpcoid  6197  dfpo2  6203  fnprb  7093  fntpb  7094  xpexr  7774  frxp  7976  suppimacnv  7999  fodomr  8924  wdompwdom  9346  en3lp  9381  inf3lemd  9394  prdom2  9771  iunfictbso  9879  infpssrlem4  10071  1re  10984  dedekindle  11148  00id  11159  nn0lt2  12392  nn01to3  12690  ioorebas  13192  fzfi  13701  ssnn0fi  13714  hash2prde  14193  repswsymballbi  14502  cshw0  14516  cshwmodn  14517  cshwsublen  14518  cshwn  14519  cshwlen  14521  cshwidx0  14528  dmtrclfv  14738  cncongr2  16382  cshwsidrepswmod0  16805  cshwshashlem1  16806  cshwshashlem2  16807  cshwsdisj  16809  cntzssv  18943  psgnunilem4  19114  sdrgacs  20078  mulmarep1gsum2  21732  plyssc  25370  cxpsqrtth  25893  addsqnreup  26600  2sqreultlem  26604  2sqreunnltlem  26607  axsegcon  27304  axpaschlem  27317  axlowdimlem16  27334  axcontlem7  27347  axcontlem8  27348  axcontlem12  27352  umgrislfupgrlem  27501  edglnl  27522  uhgr2edg  27584  1egrvtxdg0  27887  uspgrn2crct  28182  2pthon3v  28317  clwwlknon0  28466  1pthon2v  28526  1to3vfriswmgr  28653  frgrnbnb  28666  numclwwlk5  28761  siii  29224  h1de2ctlem  29926  riesz3i  30433  unierri  30475  dya2iocuni  32259  sibf0  32310  bnj1143  32779  bnj571  32895  bnj594  32901  bnj852  32910  noresle  33909  cgrextend  34319  ifscgr  34355  idinside  34395  btwnconn1lem12  34409  btwnconn1  34412  linethru  34464  bj-xpnzex  35158  ovoliunnfl  35828  voliunnfl  35830  volsupnfl  35831  sn-1ne2  40302  ax6e2ndeq  42186  lighneal  45074  nrhmzr  45442  zlmodzxznm  45849  itsclc0yqe  46118