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  4769  prnebg  4800  preqsnd  4803  preq12nebg  4807  prel12g  4808  opthprneg  4809  3elpr2eq  4850  snopeqop  5454  propssopi  5456  opthhausdorff  5465  opthhausdorff0  5466  iunopeqop  5469  tpres  7149  f1ounsn  7220  fvf1pr  7255  elovmpt3imp  7617  resf1extb  7878  bropopvvv  8033  bropfvvvvlem  8034  infsupprpr  9412  epnsym  9521  eldju2ndl  9839  eldju2ndr  9840  fin1a2lem10  10322  fvf1tp  13739  modfzo0difsn  13896  suppssfz  13947  hashrabsn1  14327  hash2pwpr  14429  hashle2pr  14430  hashge2el2difr  14434  cshwidxmod  14756  cshwidx0  14759  mod2eq1n2dvds  16307  nno  16342  prm2orodd  16651  prm23lt5  16776  dvdsprmpweqnn  16847  symgextf1  19387  01eq0ringOLD  20499  nzerooringczr  21470  mamufacex  22371  mavmulsolcl  22526  chfacfscmulgsum  22835  chfacfpmmulgsum  22839  logbgcd1irr  26771  lgsqrmodndvds  27330  gausslemma2dlem0f  27338  gausslemma2dlem0i  27341  2lgs  27384  2lgsoddprm  27393  2sqreultlem  27424  2sqreunnltlem  27427  ltlesnd  27753  umgrnloop2  29229  uhgr2edg  29291  uvtx01vtx  29480  g0wlk0  29734  wlkreslem  29751  upgrwlkdvdelem  29819  uspgrn2crct  29891  wspn0  30007  2pthdlem1  30013  2pthon3v  30026  umgr2adedgspth  30031  umgrclwwlkge2  30076  lppthon  30236  1pthon2v  30238  frgrwopreglem4a  30395  frgrreg  30479  frgrregord13  30481  frgrogt3nreg  30482  nsnlplig  30567  nsnlpligALT  30568  gonarlem  35592  gonar  35593  goalrlem  35594  goalr  35595  bj-prmoore  37443  prproropf1olem4  47978  paireqne  47983  goldbachth  48022  lighneallem2  48081  lighneal  48086  requad1  48110  evenltle  48205  fppr2odd  48219  elclnbgrelnbgr  48313  vopnbgrelself  48343  dfnbgr6  48345  isubgr3stgrlem4  48457  isubgr3stgrlem7  48460  gpgvtxedg0  48551  gpgvtxedg1  48552  gpgedgiov  48553  gpgedg2ov  48554  gpgedg2iv  48555  gpgprismgr4cycllem7  48589  pgnioedg1  48596  pgnioedg2  48597  pgnioedg3  48598  pgnioedg4  48599  pgnioedg5  48600  pgnbgreunbgrlem1  48601  pgnbgreunbgrlem2lem1  48602  pgnbgreunbgrlem2lem2  48603  pgnbgreunbgrlem2lem3  48604  pgnbgreunbgrlem2  48605  pgnbgreunbgrlem4  48607  pgnbgreunbgrlem5lem1  48608  pgnbgreunbgrlem5lem2  48609  pgnbgreunbgrlem5  48611  lidldomn1  48719  ztprmneprm  48835  suppmptcfin  48864  linc1  48913  lindsrng01  48956  ldepspr  48961  zlmodzxznm  48985  rrx2xpref1o  49206  rrx2plord2  49210  line2ylem  49239  line2xlem  49241  line2y  49243  inlinecirc02plem  49274