Theorem pm2.61ine 3103

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1536   ≠ wne 3019

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 209  df-ne 3020

This theorem is referenced by:  pm2.61ne  3105  pm2.61iine  3110  raaan  4463  raaanv  4464  iinrab2  4995  iinvdif  5005  riinrab  5009  reusv2lem2  5303  po2ne  5492  xpriindi  5710  dmxpid  5803  dmxpss  6031  rnxpid  6033  cnvpo  6141  xpcoid  6144  fnprb  6974  fntpb  6975  xpexr  7626  frxp  7823  suppimacnv  7844  fodomr  8671  wdompwdom  9045  en3lp  9080  inf3lemd  9093  prdom2  9435  iunfictbso  9543  infpssrlem4  9731  1re  10644  dedekindle  10807  00id  10818  nn0lt2  12048  nn01to3  12344  ioorebas  12842  fzfi  13343  ssnn0fi  13356  hash2prde  13831  repswsymballbi  14145  cshw0  14159  cshwmodn  14160  cshwsublen  14161  cshwn  14162  cshwlen  14164  cshwidx0  14171  dmtrclfv  14381  cncongr2  16015  cshwsidrepswmod0  16431  cshwshashlem1  16432  cshwshashlem2  16433  cshwsdisj  16435  cntzssv  18461  psgnunilem4  18628  sdrgacs  19583  mulmarep1gsum2  21186  plyssc  24793  cxpsqrtth  25315  addsqnreup  26022  2sqreultlem  26026  2sqreunnltlem  26029  axsegcon  26716  axpaschlem  26729  axlowdimlem16  26746  axcontlem7  26759  axcontlem8  26760  axcontlem12  26764  umgrislfupgrlem  26910  edglnl  26931  uhgr2edg  26993  1egrvtxdg0  27296  uspgrn2crct  27589  2pthon3v  27725  clwwlknon0  27875  1pthon2v  27935  1to3vfriswmgr  28062  frgrnbnb  28075  numclwwlk5  28170  siii  28633  h1de2ctlem  29335  riesz3i  29842  unierri  29884  dya2iocuni  31545  sibf0  31596  bnj1143  32066  bnj571  32182  bnj594  32188  bnj852  32197  dfpo2  32995  noresle  33204  cgrextend  33473  ifscgr  33509  idinside  33549  btwnconn1lem12  33563  btwnconn1  33566  linethru  33618  bj-xpnzex  34275  ovoliunnfl  34938  voliunnfl  34940  volsupnfl  34941  sn-1ne2  39164  ax6e2ndeq  40899  lighneal  43783  nrhmzr  44151  zlmodzxznm  44559  itsclc0yqe  44755