Theorem eqneqall 2966

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2956

This theorem is used by:  nonconne  2967  ssprsseq  4786  prnebg  4816  preqsnd  4819  preq12nebg  4823  prel12g  4824  opthprneg  4825  3elpr2eq  4866  snopeqop  5483  propssopi  5485  opthhausdorff  5494  opthhausdorff0  5495  iunopeqop  5498  iunopeqopOLD  5499  tpres  7200  f1ounsn  7273  fvf1pr  7308  elovmpt3imp  7671  resf1extb  7931  bropopvvv  8087  bropfvvvvlem  8088  infsupprpr  9476  epnsym  9588  eldju2ndl  9929  eldju2ndr  9930  fin1a2lem10  10411  fvf1tp  13850  modfzo0difsn  14007  suppssfz  14058  hashrabsn1  14438  hash2pwpr  14541  hashle2pr  14542  hashge2el2difr  14546  cshwidxmod  14874  cshwidx0  14877  mod2eq1n2dvds  16437  nno  16472  prm2orodd  16781  prm23lt5  16906  dvdsprmpweqnn  16977  symgextf1  19548  01eq0ringOLD  20692  nzerooringczr  21693  mamufacex  22618  mavmulsolcl  22773  chfacfscmulgsum  23085  chfacfpmmulgsum  23089  logbgcd1irr  27031  lgsqrmodndvds  27589  gausslemma2dlem0f  27597  gausslemma2dlem0i  27600  2lgs  27643  2lgsoddprm  27652  2sqreultlem  27683  2sqreunnltlem  27686  ltlesnd  28011  umgrnloop2  29603  uhgr2edg  29668  uvtx01vtx  29857  g0wlk0  30110  wlkreslem  30127  upgrwlkdvdelem  30201  uspgrn2crct  30276  wspn0  30392  2pthdlem1  30398  2pthon3v  30411  umgr2adedgspth  30416  umgrclwwlkge2  30461  lppthon  30621  1pthon2v  30633  frgrwopreglem4a  30790  frgrreg  30874  frgrregord13  30876  frgrogt3nreg  30877  nsnlplig  30962  nsnlpligALT  30963  gonarlem  35973  gonar  35974  goalrlem  35975  goalr  35976  bj-prmoore  37865  prproropf1olem4  48406  paireqne  48411  goldbachth  48450  lighneallem2  48509  lighneal  48514  requad1  48538  evenltle  48633  fppr2odd  48647  elclnbgrelnbgr  48741  vopnbgrelself  48771  dfnbgr6  48773  isubgr3stgrlem4  48885  isubgr3stgrlem7  48888  gpgvtxedg0  48979  gpgvtxedg1  48980  gpgedgiov  48981  gpgedg2ov  48982  gpgedg2iv  48983  gpgprismgr4cycllem7  49017  pgnioedg1  49024  pgnioedg2  49025  pgnioedg3  49026  pgnioedg4  49027  pgnioedg5  49028  pgnbgreunbgrlem1  49029  pgnbgreunbgrlem2lem1  49030  pgnbgreunbgrlem2lem2  49031  pgnbgreunbgrlem2lem3  49032  pgnbgreunbgrlem2  49033  pgnbgreunbgrlem4  49035  pgnbgreunbgrlem5lem1  49036  pgnbgreunbgrlem5lem2  49037  pgnbgreunbgrlem5  49039  lidldomn1  49146  ztprmneprm  49277  suppmptcfin  49306  linc1  49355  lindsrng01  49398  ldepspr  49403  zlmodzxznm  49427  rrx2xpref1o  49648  rrx2plord2  49652  line2ylem  49681  line2xlem  49683  line2y  49685  inlinecirc02plem  49716