Theorem pm2.61ine 2906

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1523   ≠ wne 2823

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 197  df-ne 2824

This theorem is referenced by:  pm2.61ne  2908  pm2.61iine  2913  rgenzOLD  4110  raaan  4115  iinrab2  4615  iinvdif  4624  riinrab  4628  reusv2lem2  4899  reusv2lem2OLD  4900  xpriindi  5291  dmxpid  5377  dmxpss  5600  rnxpid  5602  cnvpo  5711  xpcoid  5714  fnprb  6513  fntpb  6514  xpexr  7148  frxp  7332  suppimacnv  7351  fodomr  8152  wdompwdom  8524  en3lp  8551  inf3lemd  8562  prdom2  8867  iunfictbso  8975  infpssrlem4  9166  1re  10077  dedekindle  10239  00id  10249  nn0lt2  11478  nn01to3  11819  ioorebas  12313  fzfi  12811  ssnn0fi  12824  hash2prde  13290  repswsymballbi  13573  cshw0  13586  cshwmodn  13587  cshwsublen  13588  cshwn  13589  cshwlen  13591  cshwidx0  13598  dmtrclfv  13803  cncongr2  15429  cshwsidrepswmod0  15848  cshwshashlem1  15849  cshwshashlem2  15850  cshwsdisj  15852  cntzssv  17807  psgnunilem4  17963  mulmarep1gsum2  20428  plyssc  24001  axsegcon  25852  axpaschlem  25865  axlowdimlem16  25882  axcontlem7  25895  axcontlem8  25896  axcontlem12  25900  umgrislfupgrlem  26062  edglnl  26083  uhgr2edg  26145  1egrvtxdg0  26463  uspgrn2crct  26756  2pthon3v  26908  clwwlknon0  27068  1pthon2v  27131  1to3vfriswmgr  27260  frgrnbnb  27273  numclwwlk5  27375  siii  27836  h1de2ctlem  28542  riesz3i  29049  unierri  29091  dya2iocuni  30473  sibf0  30524  bnj1143  30987  bnj571  31102  bnj594  31108  bnj852  31117  dfpo2  31771  noresle  31971  cgrextend  32240  ifscgr  32276  idinside  32316  btwnconn1lem12  32330  btwnconn1  32333  linethru  32385  bj-xpnzex  33071  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  sdrgacs  38088  ax6e2ndeq  39092  lighneal  41853  nrhmzr  42198  zlmodzxznm  42611