Theorem pm2.61ine 3011

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 2932	. . 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 1541   ≠ wne 2928

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 2929

This theorem is referenced by:  pm2.61ne  3013  pm2.61dne  3014  pm2.61iine  3018  raaan  4464  raaanv  4465  iinrab2  5016  iinvdif  5026  riinrab  5030  reusv2lem2  5335  po2ne  5538  xpriindi  5775  dmxpid  5869  dmxpss  6118  rnxpid  6120  cnvpo  6234  xpcoid  6237  dfpo2  6243  fnprb  7142  fntpb  7143  xpexr  7848  frxp  8056  suppimacnv  8104  fodomr  9041  fodomfir  9212  wdompwdom  9464  en3lp  9504  inf3lemd  9517  prdom2  9897  iunfictbso  10005  infpssrlem4  10197  1re  11112  dedekindle  11277  00id  11288  nn0lt2  12536  nn01to3  12839  ioorebas  13351  fzfi  13879  ssnn0fi  13892  hash2prde  14377  repswsymballbi  14687  cshw0  14701  cshwmodn  14702  cshwsublen  14703  cshwn  14704  cshwlen  14706  cshwidx0  14713  dmtrclfv  14925  cncongr2  16579  cshwsidrepswmod0  17006  cshwshashlem1  17007  cshwshashlem2  17008  cshwsdisj  17010  cntzssv  19240  psgnunilem4  19409  nrhmzr  20452  sdrgacs  20716  mulmarep1gsum2  22489  plyssc  26132  cxpsqrtth  26666  addsqnreup  27381  2sqreultlem  27385  2sqreunnltlem  27388  noresle  27636  onscutlt  28201  n0sfincut  28282  axsegcon  28905  axpaschlem  28918  axlowdimlem16  28935  axcontlem7  28948  axcontlem8  28949  axcontlem12  28953  umgrislfupgrlem  29100  edglnl  29121  uhgr2edg  29186  1egrvtxdg0  29490  dfpth2  29707  uspgrn2crct  29786  2pthon3v  29921  clwwlknon0  30073  1pthon2v  30133  1to3vfriswmgr  30260  frgrnbnb  30273  numclwwlk5  30368  siii  30833  h1de2ctlem  31535  riesz3i  32042  unierri  32084  dya2iocuni  34296  sibf0  34347  bnj1143  34802  bnj571  34918  bnj594  34924  bnj852  34933  cgrextend  36052  ifscgr  36088  idinside  36128  btwnconn1lem12  36142  btwnconn1  36145  linethru  36197  bj-xpnzex  37003  ovoliunnfl  37712  voliunnfl  37714  volsupnfl  37715  sn-1ne2  42368  cantnfresb  43427  ax6e2ndeq  44662  lighneal  47721  dfclnbgr6  47966  dfsclnbgr6  47968  gpg5nbgrvtx03starlem1  48178  gpg5nbgrvtx03starlem2  48179  gpg5nbgrvtx03starlem3  48180  gpg5nbgrvtx13starlem1  48181  gpg5nbgrvtx13starlem2  48182  gpg5nbgrvtx13starlem3  48183  gpg5edgnedg  48240  zlmodzxznm  48608  itsclc0yqe  48872  reldmlan2  49728  reldmran2  49729  rellan  49734  relran  49735