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 1540   ≠ 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  4492  raaanv  4493  iinrab2  5046  iinvdif  5056  riinrab  5060  reusv2lem2  5369  po2ne  5577  xpriindi  5816  dmxpid  5910  dmxpss  6160  rnxpid  6162  cnvpo  6276  xpcoid  6279  dfpo2  6285  fnprb  7200  fntpb  7201  xpexr  7914  frxp  8125  suppimacnv  8173  fodomr  9142  fodomfir  9340  wdompwdom  9592  en3lp  9628  inf3lemd  9641  prdom2  10020  iunfictbso  10128  infpssrlem4  10320  1re  11235  dedekindle  11399  00id  11410  nn0lt2  12656  nn01to3  12957  ioorebas  13468  fzfi  13990  ssnn0fi  14003  hash2prde  14488  repswsymballbi  14798  cshw0  14812  cshwmodn  14813  cshwsublen  14814  cshwn  14815  cshwlen  14817  cshwidx0  14824  dmtrclfv  15037  cncongr2  16687  cshwsidrepswmod0  17114  cshwshashlem1  17115  cshwshashlem2  17116  cshwsdisj  17118  cntzssv  19311  psgnunilem4  19478  nrhmzr  20497  sdrgacs  20761  mulmarep1gsum2  22512  plyssc  26157  cxpsqrtth  26691  addsqnreup  27406  2sqreultlem  27410  2sqreunnltlem  27413  noresle  27661  onscutlt  28217  n0sfincut  28298  axsegcon  28906  axpaschlem  28919  axlowdimlem16  28936  axcontlem7  28949  axcontlem8  28950  axcontlem12  28954  umgrislfupgrlem  29101  edglnl  29122  uhgr2edg  29187  1egrvtxdg0  29491  dfpth2  29711  uspgrn2crct  29790  2pthon3v  29925  clwwlknon0  30074  1pthon2v  30134  1to3vfriswmgr  30261  frgrnbnb  30274  numclwwlk5  30369  siii  30834  h1de2ctlem  31536  riesz3i  32043  unierri  32085  dya2iocuni  34315  sibf0  34366  bnj1143  34821  bnj571  34937  bnj594  34943  bnj852  34952  cgrextend  36026  ifscgr  36062  idinside  36102  btwnconn1lem12  36116  btwnconn1  36119  linethru  36171  bj-xpnzex  36977  ovoliunnfl  37686  voliunnfl  37688  volsupnfl  37689  sn-1ne2  42315  cantnfresb  43348  ax6e2ndeq  44584  lighneal  47625  dfclnbgr6  47869  dfsclnbgr6  47871  gpg5nbgrvtx03starlem1  48070  gpg5nbgrvtx03starlem2  48071  gpg5nbgrvtx03starlem3  48072  gpg5nbgrvtx13starlem1  48073  gpg5nbgrvtx13starlem2  48074  gpg5nbgrvtx13starlem3  48075  zlmodzxznm  48473  itsclc0yqe  48741  reldmlan2  49492  reldmran2  49493  rellan  49498  relran  49499