Theorem eqneqall 2953

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 2943	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		pm2.24 124	. 2 ⊢ (𝐴 = 𝐵 → (¬ 𝐴 = 𝐵 → 𝜑))
3	1, 2	syl5bi 241	1 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2942

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 2943

This theorem is referenced by:  nonconne  2954  ssprsseq  4755  prnebg  4783  preqsnd  4786  preq12nebg  4790  prel12g  4791  opthprneg  4792  3elpr2eq  4835  snopeqop  5414  propssopi  5416  opthhausdorff  5425  opthhausdorff0  5426  iunopeqop  5429  tpres  7058  elovmpt3imp  7504  bropopvvv  7901  bropfvvvvlem  7902  infsupprpr  9193  epnsym  9297  eldju2ndl  9613  eldju2ndr  9614  fin1a2lem10  10096  modfzo0difsn  13591  suppssfz  13642  hashrabsn1  14017  hash2pwpr  14118  hashle2pr  14119  hashge2el2difr  14123  cshwidxmod  14444  cshwidx0  14447  mod2eq1n2dvds  15984  nno  16019  prm2orodd  16324  prm23lt5  16443  dvdsprmpweqnn  16514  symgextf1  18944  01eq0ring  20456  mamufacex  21448  mavmulsolcl  21608  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  logbgcd1irr  25849  lgsqrmodndvds  26406  gausslemma2dlem0f  26414  gausslemma2dlem0i  26417  2lgs  26460  2lgsoddprm  26469  2sqreultlem  26500  2sqreunnltlem  26503  umgrnloop2  27419  uhgr2edg  27478  uvtx01vtx  27667  g0wlk0  27921  wlkreslem  27939  upgrwlkdvdelem  28005  uspgrn2crct  28074  wspn0  28190  2pthdlem1  28196  2pthon3v  28209  umgr2adedgspth  28214  umgrclwwlkge2  28256  lppthon  28416  1pthon2v  28418  frgrwopreglem4a  28575  frgrreg  28659  frgrregord13  28661  frgrogt3nreg  28662  nsnlplig  28744  nsnlpligALT  28745  gonarlem  33256  gonar  33257  goalrlem  33258  goalr  33259  bj-prmoore  35213  prproropf1olem4  44846  paireqne  44851  goldbachth  44887  lighneallem2  44946  lighneal  44951  requad1  44962  evenltle  45057  fppr2odd  45071  lidldomn1  45367  nzerooringczr  45518  ztprmneprm  45571  suppmptcfin  45603  linc1  45654  lindsrng01  45697  ldepspr  45702  zlmodzxznm  45726  rrx2xpref1o  45952  rrx2plord2  45956  line2ylem  45985  line2xlem  45987  line2y  45989  inlinecirc02plem  46020