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 1533   ≠ 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  4751  prnebg  4779  preqsnd  4782  preq12nebg  4786  prel12g  4787  opthprneg  4788  3elpr2eq  4830  snopeqop  5388  propssopi  5390  opthhausdorff  5399  opthhausdorff0  5400  iunopeqop  5403  tpres  6957  elovmpt3imp  7396  bropopvvv  7779  bropfvvvvlem  7780  infsupprpr  8962  epnsym  9066  eldju2ndl  9347  eldju2ndr  9348  fin1a2lem10  9825  modfzo0difsn  13305  suppssfz  13356  hashrabsn1  13729  hash2pwpr  13828  hashle2pr  13829  hashge2el2difr  13833  cshwidxmod  14159  cshwidx0  14162  mod2eq1n2dvds  15690  nno  15727  prm2orodd  16029  prm23lt5  16145  dvdsprmpweqnn  16215  symgextf1  18543  01eq0ring  20039  mamufacex  20994  mavmulsolcl  21154  chfacfscmulgsum  21462  chfacfpmmulgsum  21466  logbgcd1irr  25366  lgsqrmodndvds  25923  gausslemma2dlem0f  25931  gausslemma2dlem0i  25934  2lgs  25977  2lgsoddprm  25986  2sqreultlem  26017  2sqreunnltlem  26020  umgrnloop2  26925  uhgr2edg  26984  uvtx01vtx  27173  g0wlk0  27427  wlkreslem  27445  upgrwlkdvdelem  27511  uspgrn2crct  27580  wspn0  27697  2pthdlem1  27703  2pthon3v  27716  umgr2adedgspth  27721  umgrclwwlkge2  27763  lppthon  27924  1pthon2v  27926  frgrwopreglem4a  28083  frgrreg  28167  frgrregord13  28169  frgrogt3nreg  28170  nsnlplig  28252  nsnlpligALT  28253  gonarlem  32636  gonar  32637  goalrlem  32638  goalr  32639  bj-prmoore  34401  prproropf1olem4  43662  paireqne  43667  goldbachth  43703  lighneallem2  43765  lighneal  43770  requad1  43781  evenltle  43876  fppr2odd  43890  lidldomn1  44186  nzerooringczr  44337  ztprmneprm  44389  suppmptcfin  44421  linc1  44474  lindsrng01  44517  ldepspr  44522  zlmodzxznm  44546  rrx2xpref1o  44699  rrx2plord2  44703  line2ylem  44732  line2xlem  44734  line2y  44736  inlinecirc02plem  44767