Theorem pm2.61ine 3025

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 2944	. . 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 1540   ≠ wne 2940

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 2941

This theorem is referenced by:  pm2.61ne  3027  pm2.61dne  3028  pm2.61iine  3032  raaan  4517  raaanv  4518  iinrab2  5070  iinvdif  5080  riinrab  5084  reusv2lem2  5399  po2ne  5608  xpriindi  5847  dmxpid  5941  dmxpss  6191  rnxpid  6193  cnvpo  6307  xpcoid  6310  dfpo2  6316  fnprb  7228  fntpb  7229  xpexr  7940  frxp  8151  suppimacnv  8199  fodomr  9168  fodomfir  9368  wdompwdom  9618  en3lp  9654  inf3lemd  9667  prdom2  10046  iunfictbso  10154  infpssrlem4  10346  1re  11261  dedekindle  11425  00id  11436  nn0lt2  12681  nn01to3  12983  ioorebas  13491  fzfi  14013  ssnn0fi  14026  hash2prde  14509  repswsymballbi  14818  cshw0  14832  cshwmodn  14833  cshwsublen  14834  cshwn  14835  cshwlen  14837  cshwidx0  14844  dmtrclfv  15057  cncongr2  16705  cshwsidrepswmod0  17132  cshwshashlem1  17133  cshwshashlem2  17134  cshwsdisj  17136  cntzssv  19346  psgnunilem4  19515  nrhmzr  20537  sdrgacs  20802  mulmarep1gsum2  22580  plyssc  26239  cxpsqrtth  26772  addsqnreup  27487  2sqreultlem  27491  2sqreunnltlem  27494  noresle  27742  axsegcon  28942  axpaschlem  28955  axlowdimlem16  28972  axcontlem7  28985  axcontlem8  28986  axcontlem12  28990  umgrislfupgrlem  29139  edglnl  29160  uhgr2edg  29225  1egrvtxdg0  29529  dfpth2  29749  uspgrn2crct  29828  2pthon3v  29963  clwwlknon0  30112  1pthon2v  30172  1to3vfriswmgr  30299  frgrnbnb  30312  numclwwlk5  30407  siii  30872  h1de2ctlem  31574  riesz3i  32081  unierri  32123  dya2iocuni  34285  sibf0  34336  bnj1143  34804  bnj571  34920  bnj594  34926  bnj852  34935  cgrextend  36009  ifscgr  36045  idinside  36085  btwnconn1lem12  36099  btwnconn1  36102  linethru  36154  bj-xpnzex  36960  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  sn-1ne2  42300  cantnfresb  43337  ax6e2ndeq  44579  lighneal  47598  dfclnbgr6  47842  dfsclnbgr6  47844  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029  zlmodzxznm  48414  itsclc0yqe  48682