Theorem pm2.61ine 3015

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 2936	. . 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 1541   ≠ wne 2932

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 2933

This theorem is referenced by:  pm2.61ne  3017  pm2.61dne  3018  pm2.61iine  3022  raaan  4471  raaanv  4472  iinrab2  5025  iinvdif  5035  riinrab  5039  reusv2lem2  5344  po2ne  5548  xpriindi  5785  dmxpid  5879  dmxpss  6129  rnxpid  6131  cnvpo  6245  xpcoid  6248  dfpo2  6254  fnprb  7154  fntpb  7155  xpexr  7860  frxp  8068  suppimacnv  8116  fodomr  9056  fodomfir  9228  wdompwdom  9483  en3lp  9523  inf3lemd  9536  prdom2  9916  iunfictbso  10024  infpssrlem4  10216  1re  11132  dedekindle  11297  00id  11308  nn0lt2  12555  nn01to3  12854  ioorebas  13367  fzfi  13895  ssnn0fi  13908  hash2prde  14393  repswsymballbi  14703  cshw0  14717  cshwmodn  14718  cshwsublen  14719  cshwn  14720  cshwlen  14722  cshwidx0  14729  dmtrclfv  14941  cncongr2  16595  cshwsidrepswmod0  17022  cshwshashlem1  17023  cshwshashlem2  17024  cshwsdisj  17026  cntzssv  19257  psgnunilem4  19426  nrhmzr  20470  sdrgacs  20734  mulmarep1gsum2  22518  plyssc  26161  cxpsqrtth  26695  addsqnreup  27410  2sqreultlem  27414  2sqreunnltlem  27417  noresle  27665  oncutlt  28260  n0fincut  28351  axsegcon  29000  axpaschlem  29013  axlowdimlem16  29030  axcontlem7  29043  axcontlem8  29044  axcontlem12  29048  umgrislfupgrlem  29195  edglnl  29216  uhgr2edg  29281  1egrvtxdg0  29585  dfpth2  29802  uspgrn2crct  29881  2pthon3v  30016  clwwlknon0  30168  1pthon2v  30228  1to3vfriswmgr  30355  frgrnbnb  30368  numclwwlk5  30463  siii  30928  h1de2ctlem  31630  riesz3i  32137  unierri  32179  dya2iocuni  34440  sibf0  34491  bnj1143  34946  bnj571  35062  bnj594  35068  bnj852  35077  cgrextend  36202  ifscgr  36238  idinside  36278  btwnconn1lem12  36292  btwnconn1  36295  linethru  36347  bj-xpnzex  37160  ovoliunnfl  37863  voliunnfl  37865  volsupnfl  37866  sn-1ne2  42520  cantnfresb  43566  ax6e2ndeq  44800  lighneal  47857  dfclnbgr6  48102  dfsclnbgr6  48104  gpg5nbgrvtx03starlem1  48314  gpg5nbgrvtx03starlem2  48315  gpg5nbgrvtx03starlem3  48316  gpg5nbgrvtx13starlem1  48317  gpg5nbgrvtx13starlem2  48318  gpg5nbgrvtx13starlem3  48319  gpg5edgnedg  48376  zlmodzxznm  48743  itsclc0yqe  49007  reldmlan2  49862  reldmran2  49863  rellan  49868  relran  49869