Theorem pm2.61ine 3031

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 2950	. . 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 1537   ≠ wne 2946

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 2947

This theorem is referenced by:  pm2.61ne  3033  pm2.61dne  3034  pm2.61iine  3038  raaan  4540  raaanv  4541  iinrab2  5093  iinvdif  5103  riinrab  5107  reusv2lem2  5417  po2ne  5624  xpriindi  5861  dmxpid  5955  dmxpss  6202  rnxpid  6204  cnvpo  6318  xpcoid  6321  dfpo2  6327  fnprb  7245  fntpb  7246  xpexr  7958  frxp  8167  suppimacnv  8215  fodomr  9194  fodomfir  9396  wdompwdom  9647  en3lp  9683  inf3lemd  9696  prdom2  10075  iunfictbso  10183  infpssrlem4  10375  1re  11290  dedekindle  11454  00id  11465  nn0lt2  12706  nn01to3  13006  ioorebas  13511  fzfi  14023  ssnn0fi  14036  hash2prde  14519  repswsymballbi  14828  cshw0  14842  cshwmodn  14843  cshwsublen  14844  cshwn  14845  cshwlen  14847  cshwidx0  14854  dmtrclfv  15067  cncongr2  16715  cshwsidrepswmod0  17142  cshwshashlem1  17143  cshwshashlem2  17144  cshwsdisj  17146  cntzssv  19368  psgnunilem4  19539  nrhmzr  20563  sdrgacs  20824  mulmarep1gsum2  22601  plyssc  26259  cxpsqrtth  26790  addsqnreup  27505  2sqreultlem  27509  2sqreunnltlem  27512  noresle  27760  axsegcon  28960  axpaschlem  28973  axlowdimlem16  28990  axcontlem7  29003  axcontlem8  29004  axcontlem12  29008  umgrislfupgrlem  29157  edglnl  29178  uhgr2edg  29243  1egrvtxdg0  29547  uspgrn2crct  29841  2pthon3v  29976  clwwlknon0  30125  1pthon2v  30185  1to3vfriswmgr  30312  frgrnbnb  30325  numclwwlk5  30420  siii  30885  h1de2ctlem  31587  riesz3i  32094  unierri  32136  dya2iocuni  34248  sibf0  34299  bnj1143  34766  bnj571  34882  bnj594  34888  bnj852  34897  cgrextend  35972  ifscgr  36008  idinside  36048  btwnconn1lem12  36062  btwnconn1  36065  linethru  36117  bj-xpnzex  36925  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  sn-1ne2  42254  cantnfresb  43286  ax6e2ndeq  44530  lighneal  47485  dfclnbgr6  47728  dfsclnbgr6  47730  zlmodzxznm  48226  itsclc0yqe  48495