Theorem eqneqall 2943

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2932

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 2933

This theorem is referenced by:  nonconne  2944  ssprsseq  4801  prnebg  4832  preqsnd  4835  preq12nebg  4839  prel12g  4840  opthprneg  4841  3elpr2eq  4882  snopeqop  5481  propssopi  5483  opthhausdorff  5492  opthhausdorff0  5493  iunopeqop  5496  tpres  7193  f1ounsn  7265  fvf1pr  7300  elovmpt3imp  7664  resf1extb  7930  bropopvvv  8089  bropfvvvvlem  8090  infsupprpr  9518  epnsym  9623  eldju2ndl  9938  eldju2ndr  9939  fin1a2lem10  10423  fvf1tp  13806  modfzo0difsn  13961  suppssfz  14012  hashrabsn1  14392  hash2pwpr  14494  hashle2pr  14495  hashge2el2difr  14499  cshwidxmod  14821  cshwidx0  14824  mod2eq1n2dvds  16366  nno  16401  prm2orodd  16710  prm23lt5  16834  dvdsprmpweqnn  16905  symgextf1  19402  01eq0ringOLD  20491  nzerooringczr  21441  mamufacex  22334  mavmulsolcl  22489  chfacfscmulgsum  22798  chfacfpmmulgsum  22802  logbgcd1irr  26756  lgsqrmodndvds  27316  gausslemma2dlem0f  27324  gausslemma2dlem0i  27327  2lgs  27370  2lgsoddprm  27379  2sqreultlem  27410  2sqreunnltlem  27413  sltlend  27735  umgrnloop2  29125  uhgr2edg  29187  uvtx01vtx  29376  g0wlk0  29632  wlkreslem  29649  upgrwlkdvdelem  29718  uspgrn2crct  29790  wspn0  29906  2pthdlem1  29912  2pthon3v  29925  umgr2adedgspth  29930  umgrclwwlkge2  29972  lppthon  30132  1pthon2v  30134  frgrwopreglem4a  30291  frgrreg  30375  frgrregord13  30377  frgrogt3nreg  30378  nsnlplig  30462  nsnlpligALT  30463  gonarlem  35416  gonar  35417  goalrlem  35418  goalr  35419  bj-prmoore  37133  prproropf1olem4  47520  paireqne  47525  goldbachth  47561  lighneallem2  47620  lighneal  47625  requad1  47636  evenltle  47731  fppr2odd  47745  elclnbgrelnbgr  47839  vopnbgrelself  47868  dfnbgr6  47870  isubgr3stgrlem4  47981  isubgr3stgrlem7  47984  gpgvtxedg0  48067  gpgvtxedg1  48068  gpgprismgr4cycllem7  48100  lidldomn1  48206  ztprmneprm  48322  suppmptcfin  48351  linc1  48401  lindsrng01  48444  ldepspr  48449  zlmodzxznm  48473  rrx2xpref1o  48698  rrx2plord2  48702  line2ylem  48731  line2xlem  48733  line2y  48735  inlinecirc02plem  48766