Theorem eqneqall 2943

Description: A contradiction concerning equality implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)

Assertion

Ref	Expression
eqneqall	⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜑))

Proof of Theorem eqneqall

Step	Hyp	Ref	Expression
1		df-ne 2933	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		pm2.24 124	. 2 ⊢ (𝐴 = 𝐵 → (¬ 𝐴 = 𝐵 → 𝜑))
3	1, 2	biimtrid 242	1 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ 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:  nonconne  2944  ssprsseq  4781  prnebg  4812  preqsnd  4815  preq12nebg  4819  prel12g  4820  opthprneg  4821  3elpr2eq  4862  snopeqop  5454  propssopi  5456  opthhausdorff  5465  opthhausdorff0  5466  iunopeqop  5469  tpres  7147  f1ounsn  7218  fvf1pr  7253  elovmpt3imp  7615  resf1extb  7876  bropopvvv  8032  bropfvvvvlem  8033  infsupprpr  9409  epnsym  9518  eldju2ndl  9836  eldju2ndr  9837  fin1a2lem10  10319  fvf1tp  13709  modfzo0difsn  13866  suppssfz  13917  hashrabsn1  14297  hash2pwpr  14399  hashle2pr  14400  hashge2el2difr  14404  cshwidxmod  14726  cshwidx0  14729  mod2eq1n2dvds  16274  nno  16309  prm2orodd  16618  prm23lt5  16742  dvdsprmpweqnn  16813  symgextf1  19350  01eq0ringOLD  20464  nzerooringczr  21435  mamufacex  22340  mavmulsolcl  22495  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  logbgcd1irr  26760  lgsqrmodndvds  27320  gausslemma2dlem0f  27328  gausslemma2dlem0i  27331  2lgs  27374  2lgsoddprm  27383  2sqreultlem  27414  2sqreunnltlem  27417  ltlesnd  27743  umgrnloop2  29219  uhgr2edg  29281  uvtx01vtx  29470  g0wlk0  29724  wlkreslem  29741  upgrwlkdvdelem  29809  uspgrn2crct  29881  wspn0  29997  2pthdlem1  30003  2pthon3v  30016  umgr2adedgspth  30021  umgrclwwlkge2  30066  lppthon  30226  1pthon2v  30228  frgrwopreglem4a  30385  frgrreg  30469  frgrregord13  30471  frgrogt3nreg  30472  nsnlplig  30556  nsnlpligALT  30557  gonarlem  35588  gonar  35589  goalrlem  35590  goalr  35591  bj-prmoore  37320  prproropf1olem4  47752  paireqne  47757  goldbachth  47793  lighneallem2  47852  lighneal  47857  requad1  47868  evenltle  47963  fppr2odd  47977  elclnbgrelnbgr  48071  vopnbgrelself  48101  dfnbgr6  48103  isubgr3stgrlem4  48215  isubgr3stgrlem7  48218  gpgvtxedg0  48309  gpgvtxedg1  48310  gpgedgiov  48311  gpgedg2ov  48312  gpgedg2iv  48313  gpgprismgr4cycllem7  48347  pgnioedg1  48354  pgnioedg2  48355  pgnioedg3  48356  pgnioedg4  48357  pgnioedg5  48358  pgnbgreunbgrlem1  48359  pgnbgreunbgrlem2lem1  48360  pgnbgreunbgrlem2lem2  48361  pgnbgreunbgrlem2lem3  48362  pgnbgreunbgrlem2  48363  pgnbgreunbgrlem4  48365  pgnbgreunbgrlem5lem1  48366  pgnbgreunbgrlem5lem2  48367  pgnbgreunbgrlem5  48369  lidldomn1  48477  ztprmneprm  48593  suppmptcfin  48622  linc1  48671  lindsrng01  48714  ldepspr  48719  zlmodzxznm  48743  rrx2xpref1o  48964  rrx2plord2  48968  line2ylem  48997  line2xlem  48999  line2y  49001  inlinecirc02plem  49032