Theorem pm2.61ine 3082

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1656   ≠ wne 2999

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 199  df-ne 3000

This theorem is referenced by:  pm2.61ne  3084  pm2.61iine  3089  raaan  4304  iinrab2  4805  iinvdif  4814  riinrab  4818  reusv2lem2  5101  po2ne  5280  xpriindi  5495  dmxpid  5581  dmxpss  5810  rnxpid  5812  cnvpo  5918  xpcoid  5921  fnprb  6733  fntpb  6734  xpexr  7373  frxp  7556  suppimacnv  7575  fodomr  8386  wdompwdom  8759  en3lp  8793  inf3lemd  8808  prdom2  9149  iunfictbso  9257  infpssrlem4  9450  1re  10363  dedekindle  10527  00id  10537  nn0lt2  11775  nn01to3  12071  ioorebas  12571  fzfi  13073  ssnn0fi  13086  hash2prde  13548  repswsymballbi  13903  cshw0  13922  cshwmodn  13923  cshwsublen  13924  cshwn  13925  cshwlen  13927  cshwidx0  13934  dmtrclfv  14143  cncongr2  15761  cshwsidrepswmod0  16174  cshwshashlem1  16175  cshwshashlem2  16176  cshwsdisj  16178  cntzssv  18118  psgnunilem4  18275  mulmarep1gsum2  20755  plyssc  24362  cxpsqrtth  24881  axsegcon  26233  axpaschlem  26246  axlowdimlem16  26263  axcontlem7  26276  axcontlem8  26277  axcontlem12  26281  umgrislfupgrlem  26427  edglnl  26449  uhgr2edg  26511  1egrvtxdg0  26816  uspgrn2crct  27114  2pthon3v  27279  clwwlknon0  27464  1pthon2v  27525  1to3vfriswmgr  27657  frgrnbnb  27670  numclwwlk5  27799  siii  28259  h1de2ctlem  28965  riesz3i  29472  unierri  29514  dya2iocuni  30886  sibf0  30937  bnj1143  31403  bnj571  31518  bnj594  31524  bnj852  31533  dfpo2  32183  noresle  32380  cgrextend  32649  ifscgr  32685  idinside  32725  btwnconn1lem12  32739  btwnconn1  32742  linethru  32794  bj-xpnzex  33463  ovoliunnfl  33990  voliunnfl  33992  volsupnfl  33993  sdrgacs  38609  ax6e2ndeq  39598  lighneal  42372  nrhmzr  42734  zlmodzxznm  43147