Theorem pm2.61ine 3040

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1560   ≠ wne 2957

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 209  df-ne 2958

This theorem is referenced by:  pm2.61ne  3042  pm2.61dne  3043  pm2.61iine  3047  raaan  4472  raaanv  4473  iinrab2  5027  iinvdif  5037  riinrab  5041  reusv2lem2  5356  iunopeqop  5490  po2ne  5571  xpriindi  5808  dmxpid  5906  dmxpss  6157  rnxpid  6159  cnvpo  6274  xpcoid  6277  dfpo2  6283  fnprb  7192  fntpb  7193  xpexr  7899  frxp  8106  suppimacnv  8154  fodomr  9100  fodomfir  9272  wdompwdom  9526  en3lp  9569  inf3lemd  9582  prdom2  9962  iunfictbso  10070  infpssrlem4  10263  1re  11181  dedekindle  11347  00id  11358  nn0lt2  12636  nn01to3  12942  ioorebas  13455  fzfi  13985  ssnn0fi  13998  hash2prde  14483  repswsymballbi  14793  cshw0  14807  cshwmodn  14808  cshwsublen  14809  cshwn  14810  cshwlen  14812  cshwidx0  14819  dmtrclfv  15031  cncongr2  16702  cshwsidrepswmod0  17130  cshwshashlem1  17131  cshwshashlem2  17132  cshwsdisj  17134  cntzssv  19368  psgnunilem4  19537  nrhmzr  20587  sdrgacs  20850  mulmarep1gsum2  22634  plyssc  26260  cxpsqrtth  26795  addsqnreup  27507  2sqreultlem  27511  2sqreunnltlem  27514  noresle  27761  oncutlt  28357  n0fincut  28448  axsegcon  29128  axpaschlem  29141  axlowdimlem16  29158  axcontlem7  29171  axcontlem8  29172  axcontlem12  29176  umgrislfupgrlem  29323  edglnl  29344  uhgr2edg  29409  1egrvtxdg0  29712  dfpth2  29929  uspgrn2crct  30008  2pthon3v  30143  clwwlknon0  30295  1pthon2v  30355  1to3vfriswmgr  30482  frgrnbnb  30495  numclwwlk5  30590  siii  31056  h1de2ctlem  31758  riesz3i  32265  unierri  32307  dya2iocuni  34580  sibf0  34631  bnj1143  35085  bnj571  35201  bnj594  35207  bnj852  35216  cgrextend  36358  ifscgr  36394  idinside  36434  btwnconn1lem12  36448  btwnconn1  36451  linethru  36503  bj-xpnzex  37444  ovoliunnfl  38161  voliunnfl  38163  volsupnfl  38164  sn-1ne2  42880  cantnfresb  43901  ax6e2ndeq  45135  lighneal  48220  dfclnbgr6  48478  dfsclnbgr6  48480  gpg5nbgrvtx03starlem1  48690  gpg5nbgrvtx03starlem2  48691  gpg5nbgrvtx03starlem3  48692  gpg5nbgrvtx13starlem1  48693  gpg5nbgrvtx13starlem2  48694  gpg5nbgrvtx13starlem3  48695  gpg5edgnedg  48752  zlmodzxznm  49119  itsclc0yqe  49383  reldmlan2  50238  reldmran2  50239  rellan  50244  relran  50245