Theorem pm2.61ine 3016

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 2937	. . 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 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  pm2.61ne  3018  pm2.61dne  3019  pm2.61iine  3023  raaan  4459  raaanv  4460  iinrab2  5013  iinvdif  5023  riinrab  5027  reusv2lem2  5337  po2ne  5549  xpriindi  5786  dmxpid  5880  dmxpss  6130  rnxpid  6132  cnvpo  6246  xpcoid  6249  dfpo2  6255  fnprb  7157  fntpb  7158  xpexr  7863  frxp  8070  suppimacnv  8118  fodomr  9060  fodomfir  9232  wdompwdom  9487  en3lp  9529  inf3lemd  9542  prdom2  9922  iunfictbso  10030  infpssrlem4  10222  1re  11138  dedekindle  11304  00id  11315  nn0lt2  12586  nn01to3  12885  ioorebas  13398  fzfi  13928  ssnn0fi  13941  hash2prde  14426  repswsymballbi  14736  cshw0  14750  cshwmodn  14751  cshwsublen  14752  cshwn  14753  cshwlen  14755  cshwidx0  14762  dmtrclfv  14974  cncongr2  16631  cshwsidrepswmod0  17059  cshwshashlem1  17060  cshwshashlem2  17061  cshwsdisj  17063  cntzssv  19297  psgnunilem4  19466  nrhmzr  20508  sdrgacs  20772  mulmarep1gsum2  22552  plyssc  26178  cxpsqrtth  26710  addsqnreup  27423  2sqreultlem  27427  2sqreunnltlem  27430  noresle  27678  oncutlt  28273  n0fincut  28364  axsegcon  29013  axpaschlem  29026  axlowdimlem16  29043  axcontlem7  29056  axcontlem8  29057  axcontlem12  29061  umgrislfupgrlem  29208  edglnl  29229  uhgr2edg  29294  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  34446  sibf0  34497  bnj1143  34951  bnj571  35067  bnj594  35073  bnj852  35082  cgrextend  36209  ifscgr  36245  idinside  36285  btwnconn1lem12  36299  btwnconn1  36302  linethru  36354  bj-xpnzex  37285  ovoliunnfl  38000  voliunnfl  38002  volsupnfl  38003  sn-1ne2  42720  cantnfresb  43773  ax6e2ndeq  45007  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