Theorem pm2.61ine 2865

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ≠ wne 2780

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 196  df-ne 2782

This theorem is referenced by:  pm2.61ne  2867  pm2.61iine  2872  rgenzOLD  4029  raaan  4032  iinrab2  4519  iinvdif  4528  riinrab  4532  reusv2lem2  4795  reusv2lem2OLD  4796  xpriindi  5180  dmxpid  5266  dmxpss  5484  rnxpid  5486  cnvpo  5590  xpcoid  5593  fnprb  6377  fntpb  6378  xpexr  6999  frxp  7174  suppimacnv  7193  fodomr  7996  wdompwdom  8366  en3lp  8396  inf3lemd  8407  prdom2  8712  iunfictbso  8820  infpssrlem4  9011  1re  9918  dedekindle  10080  00id  10090  nn0lt2  11317  nn01to3  11657  ioorebas  12146  fzfi  12633  ssnn0fi  12646  hash2prde  13109  repswsymballbi  13378  cshw0  13391  cshwmodn  13392  cshwsublen  13393  cshwn  13394  cshwlen  13396  cshwidx0  13403  dmtrclfv  13607  cncongr2  15220  cshwsidrepswmod0  15639  cshwshashlem1  15640  cshwshashlem2  15641  cshwsdisj  15643  cntzssv  17584  psgnunilem4  17740  mulmarep1gsum2  20199  plyssc  23760  axsegcon  25607  axpaschlem  25620  axlowdimlem16  25637  axcontlem7  25650  axcontlem8  25651  axcontlem12  25655  umgrislfupgrlem  25788  usgra2edg  25911  usgrcyclnl2  26169  4cycl4dv  26195  1to3vfriswmgra  26534  frgranbnb  26547  numclwwlk5  26639  siii  27092  h1de2ctlem  27798  riesz3i  28305  unierri  28347  dya2iocuni  29672  sibf0  29723  bnj1143  30115  bnj571  30230  bnj594  30236  bnj852  30245  dfpo2  30898  cgrextend  31285  ifscgr  31321  idinside  31361  btwnconn1lem12  31375  btwnconn1  31378  linethru  31430  bj-xpnzex  32139  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  sdrgacs  36790  ax6e2ndeq  37796  lighneal  40066  uhgr2edg  40435  1egrvtxdg0  40727  uspgrn2crct  41011  2pthon3v-av  41150  1pthon2v-av  41320  1to3vfriswmgr  41450  frgrnbnb  41463  av-numclwwlk5  41542  nrhmzr  41663  zlmodzxznm  42080