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 216	. 2 ⊢ (¬ 𝐴 ≠ 𝐵 → 𝜑)
5	1, 4	pm2.61i 182	1 ⊢ 𝜑

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ 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 206  df-ne 2941

This theorem is referenced by:  pm2.61ne  3027  pm2.61dne  3028  pm2.61iine  3032  raaan  4520  raaanv  4521  iinrab2  5073  iinvdif  5083  riinrab  5087  reusv2lem2  5397  po2ne  5604  xpriindi  5836  dmxpid  5929  dmxpss  6170  rnxpid  6172  cnvpo  6286  xpcoid  6289  dfpo2  6295  fnprb  7212  fntpb  7213  xpexr  7911  frxp  8114  suppimacnv  8161  fodomr  9130  wdompwdom  9575  en3lp  9611  inf3lemd  9624  prdom2  10003  iunfictbso  10111  infpssrlem4  10303  1re  11216  dedekindle  11380  00id  11391  nn0lt2  12627  nn01to3  12927  ioorebas  13430  fzfi  13939  ssnn0fi  13952  hash2prde  14433  repswsymballbi  14732  cshw0  14746  cshwmodn  14747  cshwsublen  14748  cshwn  14749  cshwlen  14751  cshwidx0  14758  dmtrclfv  14967  cncongr2  16607  cshwsidrepswmod0  17030  cshwshashlem1  17031  cshwshashlem2  17032  cshwsdisj  17034  cntzssv  19194  psgnunilem4  19367  sdrgacs  20421  mulmarep1gsum2  22083  plyssc  25721  cxpsqrtth  26245  addsqnreup  26953  2sqreultlem  26957  2sqreunnltlem  26960  noresle  27207  axsegcon  28223  axpaschlem  28236  axlowdimlem16  28253  axcontlem7  28266  axcontlem8  28267  axcontlem12  28271  umgrislfupgrlem  28420  edglnl  28441  uhgr2edg  28503  1egrvtxdg0  28806  uspgrn2crct  29100  2pthon3v  29235  clwwlknon0  29384  1pthon2v  29444  1to3vfriswmgr  29571  frgrnbnb  29584  numclwwlk5  29679  siii  30144  h1de2ctlem  30846  riesz3i  31353  unierri  31395  dya2iocuni  33351  sibf0  33402  bnj1143  33870  bnj571  33986  bnj594  33992  bnj852  34001  cgrextend  35049  ifscgr  35085  idinside  35125  btwnconn1lem12  35139  btwnconn1  35142  linethru  35194  bj-xpnzex  35926  ovoliunnfl  36616  voliunnfl  36618  volsupnfl  36619  sn-1ne2  41261  cantnfresb  42156  ax6e2ndeq  43402  lighneal  46358  nrhmzr  46726  zlmodzxznm  47256  itsclc0yqe  47525