Theorem pm2.61ine 3017

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ≠ wne 2934

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 208  df-ne 2935

This theorem is referenced by:  pm2.61ne  3019  pm2.61dne  3020  pm2.61iine  3024  raaan  4446  raaanv  4447  iinrab2  4999  iinvdif  5009  riinrab  5013  reusv2lem2  5328  iunopeqop  5462  po2ne  5542  xpriindi  5778  dmxpid  5872  dmxpss  6122  rnxpid  6124  cnvpo  6238  xpcoid  6241  dfpo2  6247  fnprb  7152  fntpb  7153  xpexr  7858  frxp  8066  suppimacnv  8114  fodomr  9056  fodomfir  9228  wdompwdom  9483  en3lp  9526  inf3lemd  9539  prdom2  9919  iunfictbso  10027  infpssrlem4  10219  1re  11135  dedekindle  11301  00id  11312  nn0lt2  12583  nn01to3  12882  ioorebas  13395  fzfi  13925  ssnn0fi  13938  hash2prde  14423  repswsymballbi  14733  cshw0  14747  cshwmodn  14748  cshwsublen  14749  cshwn  14750  cshwlen  14752  cshwidx0  14759  dmtrclfv  14971  cncongr2  16628  cshwsidrepswmod0  17056  cshwshashlem1  17057  cshwshashlem2  17058  cshwsdisj  17060  cntzssv  19294  psgnunilem4  19463  nrhmzr  20509  sdrgacs  20773  mulmarep1gsum2  22557  plyssc  26183  cxpsqrtth  26712  addsqnreup  27424  2sqreultlem  27428  2sqreunnltlem  27431  noresle  27679  oncutlt  28274  n0fincut  28365  axsegcon  29014  axpaschlem  29027  axlowdimlem16  29044  axcontlem7  29057  axcontlem8  29058  axcontlem12  29062  umgrislfupgrlem  29209  edglnl  29230  uhgr2edg  29295  1egrvtxdg0  29598  dfpth2  29815  uspgrn2crct  29894  2pthon3v  30029  clwwlknon0  30181  1pthon2v  30241  1to3vfriswmgr  30368  frgrnbnb  30381  numclwwlk5  30476  siii  30942  h1de2ctlem  31644  riesz3i  32151  unierri  32193  dya2iocuni  34467  sibf0  34518  bnj1143  34972  bnj571  35088  bnj594  35094  bnj852  35103  cgrextend  36236  ifscgr  36272  idinside  36312  btwnconn1lem12  36326  btwnconn1  36329  linethru  36381  bj-xpnzex  37312  ovoliunnfl  38029  voliunnfl  38031  volsupnfl  38032  sn-1ne2  42748  cantnfresb  43769  ax6e2ndeq  45003  lighneal  48089  dfclnbgr6  48347  dfsclnbgr6  48349  gpg5nbgrvtx03starlem1  48559  gpg5nbgrvtx03starlem2  48560  gpg5nbgrvtx03starlem3  48561  gpg5nbgrvtx13starlem1  48562  gpg5nbgrvtx13starlem2  48563  gpg5nbgrvtx13starlem3  48564  gpg5edgnedg  48621  zlmodzxznm  48988  itsclc0yqe  49252  reldmlan2  50107  reldmran2  50108  rellan  50113  relran  50114