Theorem pm2.61ine 3026

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 2945	. . 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 1542   ≠ wne 2941

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 2942

This theorem is referenced by:  pm2.61ne  3028  pm2.61dne  3029  pm2.61iine  3033  raaan  4521  raaanv  4522  iinrab2  5074  iinvdif  5084  riinrab  5088  reusv2lem2  5398  po2ne  5605  xpriindi  5837  dmxpid  5930  dmxpss  6171  rnxpid  6173  cnvpo  6287  xpcoid  6290  dfpo2  6296  fnprb  7210  fntpb  7211  xpexr  7909  frxp  8112  suppimacnv  8159  fodomr  9128  wdompwdom  9573  en3lp  9609  inf3lemd  9622  prdom2  10001  iunfictbso  10109  infpssrlem4  10301  1re  11214  dedekindle  11378  00id  11389  nn0lt2  12625  nn01to3  12925  ioorebas  13428  fzfi  13937  ssnn0fi  13950  hash2prde  14431  repswsymballbi  14730  cshw0  14744  cshwmodn  14745  cshwsublen  14746  cshwn  14747  cshwlen  14749  cshwidx0  14756  dmtrclfv  14965  cncongr2  16605  cshwsidrepswmod0  17028  cshwshashlem1  17029  cshwshashlem2  17030  cshwsdisj  17032  cntzssv  19192  psgnunilem4  19365  sdrgacs  20417  mulmarep1gsum2  22076  plyssc  25714  cxpsqrtth  26238  addsqnreup  26946  2sqreultlem  26950  2sqreunnltlem  26953  noresle  27200  axsegcon  28185  axpaschlem  28198  axlowdimlem16  28215  axcontlem7  28228  axcontlem8  28229  axcontlem12  28233  umgrislfupgrlem  28382  edglnl  28403  uhgr2edg  28465  1egrvtxdg0  28768  uspgrn2crct  29062  2pthon3v  29197  clwwlknon0  29346  1pthon2v  29406  1to3vfriswmgr  29533  frgrnbnb  29546  numclwwlk5  29641  siii  30106  h1de2ctlem  30808  riesz3i  31315  unierri  31357  dya2iocuni  33282  sibf0  33333  bnj1143  33801  bnj571  33917  bnj594  33923  bnj852  33932  cgrextend  34980  ifscgr  35016  idinside  35056  btwnconn1lem12  35070  btwnconn1  35073  linethru  35125  bj-xpnzex  35840  ovoliunnfl  36530  voliunnfl  36532  volsupnfl  36533  sn-1ne2  41179  cantnfresb  42074  ax6e2ndeq  43320  lighneal  46279  nrhmzr  46647  zlmodzxznm  47178  itsclc0yqe  47447