Theorem pm2.61ine 3013

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 2934	. . 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 2930

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 2931

This theorem is referenced by:  pm2.61ne  3015  pm2.61dne  3016  pm2.61iine  3020  raaan  4469  raaanv  4470  iinrab2  5023  iinvdif  5033  riinrab  5037  reusv2lem2  5342  po2ne  5546  xpriindi  5783  dmxpid  5877  dmxpss  6127  rnxpid  6129  cnvpo  6243  xpcoid  6246  dfpo2  6252  fnprb  7152  fntpb  7153  xpexr  7858  frxp  8066  suppimacnv  8114  fodomr  9054  fodomfir  9226  wdompwdom  9481  en3lp  9521  inf3lemd  9534  prdom2  9914  iunfictbso  10022  infpssrlem4  10214  1re  11130  dedekindle  11295  00id  11306  nn0lt2  12553  nn01to3  12852  ioorebas  13365  fzfi  13893  ssnn0fi  13906  hash2prde  14391  repswsymballbi  14701  cshw0  14715  cshwmodn  14716  cshwsublen  14717  cshwn  14718  cshwlen  14720  cshwidx0  14727  dmtrclfv  14939  cncongr2  16593  cshwsidrepswmod0  17020  cshwshashlem1  17021  cshwshashlem2  17022  cshwsdisj  17024  cntzssv  19255  psgnunilem4  19424  nrhmzr  20468  sdrgacs  20732  mulmarep1gsum2  22516  plyssc  26159  cxpsqrtth  26693  addsqnreup  27408  2sqreultlem  27412  2sqreunnltlem  27415  noresle  27663  onscutlt  28232  n0sfincut  28315  axsegcon  28949  axpaschlem  28962  axlowdimlem16  28979  axcontlem7  28992  axcontlem8  28993  axcontlem12  28997  umgrislfupgrlem  29144  edglnl  29165  uhgr2edg  29230  1egrvtxdg0  29534  dfpth2  29751  uspgrn2crct  29830  2pthon3v  29965  clwwlknon0  30117  1pthon2v  30177  1to3vfriswmgr  30304  frgrnbnb  30317  numclwwlk5  30412  siii  30877  h1de2ctlem  31579  riesz3i  32086  unierri  32128  dya2iocuni  34389  sibf0  34440  bnj1143  34895  bnj571  35011  bnj594  35017  bnj852  35026  cgrextend  36151  ifscgr  36187  idinside  36227  btwnconn1lem12  36241  btwnconn1  36244  linethru  36296  bj-xpnzex  37103  ovoliunnfl  37802  voliunnfl  37804  volsupnfl  37805  sn-1ne2  42462  cantnfresb  43508  ax6e2ndeq  44742  lighneal  47799  dfclnbgr6  48044  dfsclnbgr6  48046  gpg5nbgrvtx03starlem1  48256  gpg5nbgrvtx03starlem2  48257  gpg5nbgrvtx03starlem3  48258  gpg5nbgrvtx13starlem1  48259  gpg5nbgrvtx13starlem2  48260  gpg5nbgrvtx13starlem3  48261  gpg5edgnedg  48318  zlmodzxznm  48685  itsclc0yqe  48949  reldmlan2  49804  reldmran2  49805  rellan  49810  relran  49811