Theorem eqneqall 3027

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 3016

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 3017

This theorem is referenced by:  nonconne  3028  ssprsseq  4758  prnebg  4786  preqsnd  4789  preq12nebg  4793  prel12g  4794  opthprneg  4795  3elpr2eq  4837  snopeqop  5396  propssopi  5398  opthhausdorff  5407  opthhausdorff0  5408  iunopeqop  5411  tpres  6963  elovmpt3imp  7402  bropopvvv  7785  bropfvvvvlem  7786  infsupprpr  8968  epnsym  9072  eldju2ndl  9353  eldju2ndr  9354  fin1a2lem10  9831  modfzo0difsn  13312  suppssfz  13363  hashrabsn1  13736  hash2pwpr  13835  hashle2pr  13836  hashge2el2difr  13840  cshwidxmod  14165  cshwidx0  14168  mod2eq1n2dvds  15696  nno  15733  prm2orodd  16035  prm23lt5  16151  dvdsprmpweqnn  16221  symgextf1  18549  01eq0ring  20045  mamufacex  21000  mavmulsolcl  21160  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  logbgcd1irr  25372  lgsqrmodndvds  25929  gausslemma2dlem0f  25937  gausslemma2dlem0i  25940  2lgs  25983  2lgsoddprm  25992  2sqreultlem  26023  2sqreunnltlem  26026  umgrnloop2  26931  uhgr2edg  26990  uvtx01vtx  27179  g0wlk0  27433  wlkreslem  27451  upgrwlkdvdelem  27517  uspgrn2crct  27586  wspn0  27703  2pthdlem1  27709  2pthon3v  27722  umgr2adedgspth  27727  umgrclwwlkge2  27769  lppthon  27930  1pthon2v  27932  frgrwopreglem4a  28089  frgrreg  28173  frgrregord13  28175  frgrogt3nreg  28176  nsnlplig  28258  nsnlpligALT  28259  gonarlem  32641  gonar  32642  goalrlem  32643  goalr  32644  bj-prmoore  34410  prproropf1olem4  43688  paireqne  43693  goldbachth  43729  lighneallem2  43791  lighneal  43796  requad1  43807  evenltle  43902  fppr2odd  43916  lidldomn1  44212  nzerooringczr  44363  ztprmneprm  44415  suppmptcfin  44447  linc1  44500  lindsrng01  44543  ldepspr  44548  zlmodzxznm  44572  rrx2xpref1o  44725  rrx2plord2  44729  line2ylem  44758  line2xlem  44760  line2y  44762  inlinecirc02plem  44793