Theorem pm2.61ine 3014

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 2935	. . 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 1539   ≠ wne 2931

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 2932

This theorem is referenced by:  pm2.61ne  3016  pm2.61dne  3017  pm2.61iine  3021  raaan  4497  raaanv  4498  iinrab2  5050  iinvdif  5060  riinrab  5064  reusv2lem2  5379  po2ne  5588  xpriindi  5827  dmxpid  5921  dmxpss  6171  rnxpid  6173  cnvpo  6287  xpcoid  6290  dfpo2  6296  fnprb  7210  fntpb  7211  xpexr  7922  frxp  8133  suppimacnv  8181  fodomr  9150  fodomfir  9350  wdompwdom  9600  en3lp  9636  inf3lemd  9649  prdom2  10028  iunfictbso  10136  infpssrlem4  10328  1re  11243  dedekindle  11407  00id  11418  nn0lt2  12664  nn01to3  12965  ioorebas  13473  fzfi  13995  ssnn0fi  14008  hash2prde  14492  repswsymballbi  14801  cshw0  14815  cshwmodn  14816  cshwsublen  14817  cshwn  14818  cshwlen  14820  cshwidx0  14827  dmtrclfv  15040  cncongr2  16688  cshwsidrepswmod0  17115  cshwshashlem1  17116  cshwshashlem2  17117  cshwsdisj  17119  cntzssv  19316  psgnunilem4  19484  nrhmzr  20506  sdrgacs  20771  mulmarep1gsum2  22529  plyssc  26176  cxpsqrtth  26709  addsqnreup  27424  2sqreultlem  27428  2sqreunnltlem  27431  noresle  27679  axsegcon  28873  axpaschlem  28886  axlowdimlem16  28903  axcontlem7  28916  axcontlem8  28917  axcontlem12  28921  umgrislfupgrlem  29068  edglnl  29089  uhgr2edg  29154  1egrvtxdg0  29458  dfpth2  29678  uspgrn2crct  29757  2pthon3v  29892  clwwlknon0  30041  1pthon2v  30101  1to3vfriswmgr  30228  frgrnbnb  30241  numclwwlk5  30336  siii  30801  h1de2ctlem  31503  riesz3i  32010  unierri  32052  dya2iocuni  34260  sibf0  34311  bnj1143  34779  bnj571  34895  bnj594  34901  bnj852  34910  cgrextend  35984  ifscgr  36020  idinside  36060  btwnconn1lem12  36074  btwnconn1  36077  linethru  36129  bj-xpnzex  36935  ovoliunnfl  37644  voliunnfl  37646  volsupnfl  37647  sn-1ne2  42279  cantnfresb  43314  ax6e2ndeq  44551  lighneal  47571  dfclnbgr6  47815  dfsclnbgr6  47817  gpg5nbgrvtx03starlem1  47997  gpg5nbgrvtx03starlem2  47998  gpg5nbgrvtx03starlem3  47999  gpg5nbgrvtx13starlem1  48000  gpg5nbgrvtx13starlem2  48001  gpg5nbgrvtx13starlem3  48002  zlmodzxznm  48387  itsclc0yqe  48655