Theorem eqneqall 2944

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  nonconne  2945  ssprsseq  4783  prnebg  4814  preqsnd  4817  preq12nebg  4821  prel12g  4822  opthprneg  4823  3elpr2eq  4864  snopeqop  5462  propssopi  5464  opthhausdorff  5473  opthhausdorff0  5474  iunopeqop  5477  tpres  7157  f1ounsn  7228  fvf1pr  7263  elovmpt3imp  7625  resf1extb  7886  bropopvvv  8042  bropfvvvvlem  8043  infsupprpr  9421  epnsym  9530  eldju2ndl  9848  eldju2ndr  9849  fin1a2lem10  10331  fvf1tp  13721  modfzo0difsn  13878  suppssfz  13929  hashrabsn1  14309  hash2pwpr  14411  hashle2pr  14412  hashge2el2difr  14416  cshwidxmod  14738  cshwidx0  14741  mod2eq1n2dvds  16286  nno  16321  prm2orodd  16630  prm23lt5  16754  dvdsprmpweqnn  16825  symgextf1  19362  01eq0ringOLD  20476  nzerooringczr  21447  mamufacex  22352  mavmulsolcl  22507  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  logbgcd1irr  26772  lgsqrmodndvds  27332  gausslemma2dlem0f  27340  gausslemma2dlem0i  27343  2lgs  27386  2lgsoddprm  27395  2sqreultlem  27426  2sqreunnltlem  27429  ltlesnd  27755  umgrnloop2  29231  uhgr2edg  29293  uvtx01vtx  29482  g0wlk0  29736  wlkreslem  29753  upgrwlkdvdelem  29821  uspgrn2crct  29893  wspn0  30009  2pthdlem1  30015  2pthon3v  30028  umgr2adedgspth  30033  umgrclwwlkge2  30078  lppthon  30238  1pthon2v  30240  frgrwopreglem4a  30397  frgrreg  30481  frgrregord13  30483  frgrogt3nreg  30484  nsnlplig  30569  nsnlpligALT  30570  gonarlem  35610  gonar  35611  goalrlem  35612  goalr  35613  bj-prmoore  37368  prproropf1olem4  47866  paireqne  47871  goldbachth  47907  lighneallem2  47966  lighneal  47971  requad1  47982  evenltle  48077  fppr2odd  48091  elclnbgrelnbgr  48185  vopnbgrelself  48215  dfnbgr6  48217  isubgr3stgrlem4  48329  isubgr3stgrlem7  48332  gpgvtxedg0  48423  gpgvtxedg1  48424  gpgedgiov  48425  gpgedg2ov  48426  gpgedg2iv  48427  gpgprismgr4cycllem7  48461  pgnioedg1  48468  pgnioedg2  48469  pgnioedg3  48470  pgnioedg4  48471  pgnioedg5  48472  pgnbgreunbgrlem1  48473  pgnbgreunbgrlem2lem1  48474  pgnbgreunbgrlem2lem2  48475  pgnbgreunbgrlem2lem3  48476  pgnbgreunbgrlem2  48477  pgnbgreunbgrlem4  48479  pgnbgreunbgrlem5lem1  48480  pgnbgreunbgrlem5lem2  48481  pgnbgreunbgrlem5  48483  lidldomn1  48591  ztprmneprm  48707  suppmptcfin  48736  linc1  48785  lindsrng01  48828  ldepspr  48833  zlmodzxznm  48857  rrx2xpref1o  49078  rrx2plord2  49082  line2ylem  49111  line2xlem  49113  line2y  49115  inlinecirc02plem  49146