Theorem pm2.61ine 3039

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2957

This theorem is used by:  pm2.61ne  3041  pm2.61dne  3042  pm2.61iine  3046  raaan  4474  raaanv  4475  iinrab2  5028  iinvdif  5040  riinrab  5044  reusv2lem2  5361  iunopeqop  5494  po2ne  5575  xpriindi  5813  dmxpid  5912  dmxpss  6163  rnxpid  6165  cnvpo  6290  xpcoid  6293  dfpo2  6299  fnprb  7214  fntpb  7215  xpexr  7930  frxp  8138  suppimacnv  8191  fodomr  9147  fodomfir  9319  wdompwdom  9572  en3lp  9615  inf3lemd  9628  prdom2  10085  iunfictbso  10193  infpssrlem4  10384  1re  11308  dedekindle  11474  00id  11485  nn0lt2  12762  nn01to3  13068  ioorebas  13582  fzfi  14115  ssnn0fi  14128  hash2prde  14615  repswsymballbi  14931  cshw0  14945  cshwmodn  14946  cshwsublen  14947  cshwn  14948  cshwlen  14950  cshwidx0  14957  dmtrclfv  15171  cncongr2  16843  cshwsidrepswmod0  17272  cshwshashlem1  17273  cshwshashlem2  17274  cshwsdisj  17276  cntzssv  19542  psgnunilem4  19711  nrhmzr  20789  sdrgacs  21058  mulmarep1gsum2  22889  plyssc  26518  cxpsqrtth  27058  addsqnreup  27770  2sqreultlem  27774  2sqreunnltlem  27777  noresle  28054  oncutlt  28650  n0fincut  28741  axsegcon  29505  axpaschlem  29518  axlowdimlem16  29535  axcontlem7  29548  axcontlem8  29549  axcontlem12  29553  umgrislfupgrlem  29700  edglnl  29721  uhgr2edg  29789  1egrvtxdg0  30092  dfpth2  30314  uspgrn2crct  30397  2pthon3v  30532  clwwlknon0  30684  1pthon2v  30754  1to3vfriswmgr  30881  frgrnbnb  30894  numclwwlk5  30989  siii  31455  h1de2ctlem  32157  riesz3i  32664  unierri  32706  dya2iocuni  34915  sibf0  34966  bnj1143  35420  bnj571  35536  bnj594  35542  bnj852  35551  cgrextend  36773  ifscgr  36809  idinside  36849  btwnconn1lem12  36863  btwnconn1  36866  linethru  36918  bj-xpnzex  37872  ovoliunnfl  38580  voliunnfl  38582  volsupnfl  38583  sn-1ne2  43330  cantnfresb  44325  ax6e2ndeq  45541  lighneal  48695  dfclnbgr6  48953  dfsclnbgr6  48955  gpg5nbgrvtx03starlem1  49165  gpg5nbgrvtx03starlem2  49166  gpg5nbgrvtx03starlem3  49167  gpg5nbgrvtx13starlem1  49168  gpg5nbgrvtx13starlem2  49169  gpg5nbgrvtx13starlem3  49170  gpg5edgnedg  49227  zlmodzxznm  49608  itsclc0yqe  49872  reldmlan2  50724  reldmran2  50725  rellan  50730  relran  50731