Theorem pm2.61ine 3024

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2939

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 206  df-ne 2940

This theorem is referenced by:  pm2.61ne  3026  pm2.61dne  3027  pm2.61iine  3031  raaan  4520  raaanv  4521  iinrab2  5073  iinvdif  5083  riinrab  5087  reusv2lem2  5397  po2ne  5604  xpriindi  5836  dmxpid  5929  dmxpss  6170  rnxpid  6172  cnvpo  6286  xpcoid  6289  dfpo2  6295  fnprb  7212  fntpb  7213  xpexr  7913  frxp  8117  suppimacnv  8164  fodomr  9134  wdompwdom  9579  en3lp  9615  inf3lemd  9628  prdom2  10007  iunfictbso  10115  infpssrlem4  10307  1re  11221  dedekindle  11385  00id  11396  nn0lt2  12632  nn01to3  12932  ioorebas  13435  fzfi  13944  ssnn0fi  13957  hash2prde  14438  repswsymballbi  14737  cshw0  14751  cshwmodn  14752  cshwsublen  14753  cshwn  14754  cshwlen  14756  cshwidx0  14763  dmtrclfv  14972  cncongr2  16612  cshwsidrepswmod0  17035  cshwshashlem1  17036  cshwshashlem2  17037  cshwsdisj  17039  cntzssv  19240  psgnunilem4  19413  nrhmzr  20433  sdrgacs  20648  mulmarep1gsum2  22397  plyssc  26053  cxpsqrtth  26579  addsqnreup  27291  2sqreultlem  27295  2sqreunnltlem  27298  noresle  27545  axsegcon  28620  axpaschlem  28633  axlowdimlem16  28650  axcontlem7  28663  axcontlem8  28664  axcontlem12  28668  umgrislfupgrlem  28817  edglnl  28838  uhgr2edg  28900  1egrvtxdg0  29203  uspgrn2crct  29497  2pthon3v  29632  clwwlknon0  29781  1pthon2v  29841  1to3vfriswmgr  29968  frgrnbnb  29981  numclwwlk5  30076  siii  30541  h1de2ctlem  31243  riesz3i  31750  unierri  31792  dya2iocuni  33748  sibf0  33799  bnj1143  34267  bnj571  34383  bnj594  34389  bnj852  34398  cgrextend  35452  ifscgr  35488  idinside  35528  btwnconn1lem12  35542  btwnconn1  35545  linethru  35597  bj-xpnzex  36307  ovoliunnfl  36997  voliunnfl  36999  volsupnfl  37000  sn-1ne2  41645  cantnfresb  42540  ax6e2ndeq  43786  lighneal  46741  zlmodzxznm  47343  itsclc0yqe  47612