Theorem pm2.61ine 3016

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 2937	. . 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 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  pm2.61ne  3018  pm2.61dne  3019  pm2.61iine  3023  raaan  4473  raaanv  4474  iinrab2  5027  iinvdif  5037  riinrab  5041  reusv2lem2  5348  po2ne  5558  xpriindi  5795  dmxpid  5889  dmxpss  6139  rnxpid  6141  cnvpo  6255  xpcoid  6258  dfpo2  6264  fnprb  7166  fntpb  7167  xpexr  7872  frxp  8080  suppimacnv  8128  fodomr  9070  fodomfir  9242  wdompwdom  9497  en3lp  9537  inf3lemd  9550  prdom2  9930  iunfictbso  10038  infpssrlem4  10230  1re  11146  dedekindle  11311  00id  11322  nn0lt2  12569  nn01to3  12868  ioorebas  13381  fzfi  13909  ssnn0fi  13922  hash2prde  14407  repswsymballbi  14717  cshw0  14731  cshwmodn  14732  cshwsublen  14733  cshwn  14734  cshwlen  14736  cshwidx0  14743  dmtrclfv  14955  cncongr2  16609  cshwsidrepswmod0  17036  cshwshashlem1  17037  cshwshashlem2  17038  cshwsdisj  17040  cntzssv  19274  psgnunilem4  19443  nrhmzr  20487  sdrgacs  20751  mulmarep1gsum2  22535  plyssc  26178  cxpsqrtth  26712  addsqnreup  27427  2sqreultlem  27431  2sqreunnltlem  27434  noresle  27682  oncutlt  28277  n0fincut  28368  axsegcon  29018  axpaschlem  29031  axlowdimlem16  29048  axcontlem7  29061  axcontlem8  29062  axcontlem12  29066  umgrislfupgrlem  29213  edglnl  29234  uhgr2edg  29299  1egrvtxdg0  29603  dfpth2  29820  uspgrn2crct  29899  2pthon3v  30034  clwwlknon0  30186  1pthon2v  30246  1to3vfriswmgr  30373  frgrnbnb  30386  numclwwlk5  30481  siii  30947  h1de2ctlem  31649  riesz3i  32156  unierri  32198  dya2iocuni  34467  sibf0  34518  bnj1143  34972  bnj571  35088  bnj594  35094  bnj852  35103  cgrextend  36230  ifscgr  36266  idinside  36306  btwnconn1lem12  36320  btwnconn1  36323  linethru  36375  bj-xpnzex  37234  ovoliunnfl  37942  voliunnfl  37944  volsupnfl  37945  sn-1ne2  42664  cantnfresb  43710  ax6e2ndeq  44944  lighneal  48000  dfclnbgr6  48245  dfsclnbgr6  48247  gpg5nbgrvtx03starlem1  48457  gpg5nbgrvtx03starlem2  48458  gpg5nbgrvtx03starlem3  48459  gpg5nbgrvtx13starlem1  48460  gpg5nbgrvtx13starlem2  48461  gpg5nbgrvtx13starlem3  48462  gpg5edgnedg  48519  zlmodzxznm  48886  itsclc0yqe  49150  reldmlan2  50005  reldmran2  50006  rellan  50011  relran  50012