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 1542   ≠ 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  4768  prnebg  4799  preqsnd  4802  preq12nebg  4806  prel12g  4807  opthprneg  4808  3elpr2eq  4849  snopeqop  5460  propssopi  5462  opthhausdorff  5471  opthhausdorff0  5472  iunopeqop  5475  iunopeqopOLD  5476  tpres  7156  f1ounsn  7227  fvf1pr  7262  elovmpt3imp  7624  resf1extb  7885  bropopvvv  8040  bropfvvvvlem  8041  infsupprpr  9419  epnsym  9530  eldju2ndl  9848  eldju2ndr  9849  fin1a2lem10  10331  fvf1tp  13748  modfzo0difsn  13905  suppssfz  13956  hashrabsn1  14336  hash2pwpr  14438  hashle2pr  14439  hashge2el2difr  14443  cshwidxmod  14765  cshwidx0  14768  mod2eq1n2dvds  16316  nno  16351  prm2orodd  16660  prm23lt5  16785  dvdsprmpweqnn  16856  symgextf1  19396  01eq0ringOLD  20508  nzerooringczr  21460  mamufacex  22361  mavmulsolcl  22516  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  logbgcd1irr  26758  lgsqrmodndvds  27316  gausslemma2dlem0f  27324  gausslemma2dlem0i  27327  2lgs  27370  2lgsoddprm  27379  2sqreultlem  27410  2sqreunnltlem  27413  ltlesnd  27739  umgrnloop2  29215  uhgr2edg  29277  uvtx01vtx  29466  g0wlk0  29719  wlkreslem  29736  upgrwlkdvdelem  29804  uspgrn2crct  29876  wspn0  29992  2pthdlem1  29998  2pthon3v  30011  umgr2adedgspth  30016  umgrclwwlkge2  30061  lppthon  30221  1pthon2v  30223  frgrwopreglem4a  30380  frgrreg  30464  frgrregord13  30466  frgrogt3nreg  30467  nsnlplig  30552  nsnlpligALT  30553  gonarlem  35576  gonar  35577  goalrlem  35578  goalr  35579  bj-prmoore  37427  prproropf1olem4  47966  paireqne  47971  goldbachth  48010  lighneallem2  48069  lighneal  48074  requad1  48098  evenltle  48193  fppr2odd  48207  elclnbgrelnbgr  48301  vopnbgrelself  48331  dfnbgr6  48333  isubgr3stgrlem4  48445  isubgr3stgrlem7  48448  gpgvtxedg0  48539  gpgvtxedg1  48540  gpgedgiov  48541  gpgedg2ov  48542  gpgedg2iv  48543  gpgprismgr4cycllem7  48577  pgnioedg1  48584  pgnioedg2  48585  pgnioedg3  48586  pgnioedg4  48587  pgnioedg5  48588  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  pgnbgreunbgrlem2  48593  pgnbgreunbgrlem4  48595  pgnbgreunbgrlem5lem1  48596  pgnbgreunbgrlem5lem2  48597  pgnbgreunbgrlem5  48599  lidldomn1  48707  ztprmneprm  48823  suppmptcfin  48852  linc1  48901  lindsrng01  48944  ldepspr  48949  zlmodzxznm  48973  rrx2xpref1o  49194  rrx2plord2  49198  line2ylem  49227  line2xlem  49229  line2y  49231  inlinecirc02plem  49262