Theorem pm2.61ine 3043

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2960

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2961

This theorem is used by:  pm2.61ne  3045  pm2.61dne  3046  pm2.61iine  3050  raaan  4481  raaanv  4482  iinrab2  5036  iinvdif  5048  riinrab  5052  reusv2lem2  5372  iunopeqop  5506  po2ne  5587  xpriindi  5824  dmxpid  5922  dmxpss  6171  rnxpid  6173  cnvpo  6292  xpcoid  6295  dfpo2  6301  fnprb  7213  fntpb  7214  xpexr  7921  frxp  8128  suppimacnv  8176  fodomr  9123  fodomfir  9294  wdompwdom  9547  en3lp  9590  inf3lemd  9603  prdom2  10006  iunfictbso  10114  infpssrlem4  10305  1re  11223  dedekindle  11389  00id  11400  nn0lt2  12675  nn01to3  12981  ioorebas  13494  fzfi  14026  ssnn0fi  14039  hash2prde  14525  repswsymballbi  14841  cshw0  14855  cshwmodn  14856  cshwsublen  14857  cshwn  14858  cshwlen  14860  cshwidx0  14867  dmtrclfv  15079  cncongr2  16748  cshwsidrepswmod0  17176  cshwshashlem1  17177  cshwshashlem2  17178  cshwsdisj  17180  cntzssv  19442  psgnunilem4  19611  nrhmzr  20686  sdrgacs  20954  mulmarep1gsum2  22781  plyssc  26408  cxpsqrtth  26946  addsqnreup  27658  2sqreultlem  27662  2sqreunnltlem  27665  noresle  27912  oncutlt  28508  n0fincut  28599  axsegcon  29332  axpaschlem  29345  axlowdimlem16  29362  axcontlem7  29375  axcontlem8  29376  axcontlem12  29380  umgrislfupgrlem  29527  edglnl  29548  uhgr2edg  29616  1egrvtxdg0  29919  dfpth2  30141  uspgrn2crct  30224  2pthon3v  30359  clwwlknon0  30511  1pthon2v  30575  1to3vfriswmgr  30702  frgrnbnb  30715  numclwwlk5  30810  siii  31276  h1de2ctlem  31978  riesz3i  32485  unierri  32527  dya2iocuni  34738  sibf0  34789  bnj1143  35243  bnj571  35359  bnj594  35365  bnj852  35374  cgrextend  36537  ifscgr  36573  idinside  36613  btwnconn1lem12  36627  btwnconn1  36630  linethru  36682  bj-xpnzex  37652  ovoliunnfl  38370  voliunnfl  38372  volsupnfl  38373  sn-1ne2  43090  cantnfresb  44109  ax6e2ndeq  45326  lighneal  48421  dfclnbgr6  48679  dfsclnbgr6  48681  gpg5nbgrvtx03starlem1  48891  gpg5nbgrvtx03starlem2  48892  gpg5nbgrvtx03starlem3  48893  gpg5nbgrvtx13starlem1  48894  gpg5nbgrvtx13starlem2  48895  gpg5nbgrvtx13starlem3  48896  gpg5edgnedg  48953  zlmodzxznm  49334  itsclc0yqe  49598  reldmlan2  50452  reldmran2  50453  rellan  50458  relran  50459