Theorem eqneqall 2954

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1631   ≠ wne 2943

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 197  df-ne 2944

This theorem is referenced by:  nonconne  2955  ssprsseq  4491  prnebg  4520  preqsnd  4523  preq12nebg  4529  prel12g  4530  opthprneg  4531  3elpr2eq  4573  snopeqop  5098  propssopi  5101  opthhausdorff  5110  opthhausdorff0  5111  iunopeqop  5114  tpres  6610  elovmpt3imp  7037  bropopvvv  7406  bropfvvvvlem  7407  epnsym  8668  eldju2ndl  8950  eldju2ndr  8951  fin1a2lem10  9433  modfzo0difsn  12950  suppssfz  13001  hashrabsn1  13365  hash2pwpr  13460  hashle2pr  13461  hashge2el2difr  13465  cshwidxmod  13758  cshwidx0  13761  mod2eq1n2dvds  15279  nno  15306  prm2orodd  15611  prm23lt5  15726  dvdsprmpweqnn  15796  symgextf1  18048  01eq0ring  19487  mamufacex  20412  mavmulsolcl  20575  chfacfscmulgsum  20885  chfacfpmmulgsum  20889  lgsqrmodndvds  25299  gausslemma2dlem0f  25307  gausslemma2dlem0i  25310  2lgs  25353  2lgsoddprm  25362  umgrnloop2  26263  uhgr2edg  26322  uvtx01vtx  26525  uvtxa01vtx0OLD  26527  g0wlk0  26783  wlkreslem  26801  upgrwlkdvdelem  26867  uspgrn2crct  26936  wspn0  27071  2pthdlem1  27077  2pthon3v  27090  umgr2adedgspth  27095  umgrclwwlkge2  27141  lppthon  27331  1pthon2v  27333  frgrwopreglem4a  27492  frgrreg  27593  frgrregord13  27595  frgrogt3nreg  27596  nsnlplig  27675  nsnlpligALT  27676  goldbachth  41987  lighneallem2  42051  lighneal  42056  evenltle  42154  lidldomn1  42449  nzerooringczr  42600  ztprmneprm  42653  suppmptcfin  42688  linc1  42742  lindsrng01  42785  ldepspr  42790  zlmodzxznm  42814