Theorem eqneqall 2970

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 2960	. 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 2959

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 2960

This theorem is used by:  nonconne  2971  ssprsseq  4786  prnebg  4816  preqsnd  4819  preq12nebg  4823  prel12g  4824  opthprneg  4825  3elpr2eq  4839  snopeqop  5485  propssopi  5487  opthhausdorff  5497  opthhausdorff0  5498  iunopeqop  5501  iunopeqopOLD  5502  tpres  7238  f1ounsn  7311  fvf1pr  7346  elovmpt3imp  7710  resf1extb  7980  bropopvvv  8136  bropfvvvvlem  8137  infsupprpr  9535  epnsym  9647  eldju2ndl  10042  eldju2ndr  10043  fin1a2lem10  10526  fvf1tp  13969  modfzo0difsn  14126  suppssfz  14177  hashrabsn1  14559  hash2pwpr  14662  hashle2pr  14663  hashge2el2difr  14667  cshwidxmod  14996  cshwidx0  14999  mod2eq1n2dvds  16561  nno  16596  prm2orodd  16910  prm23lt5  17036  dvdsprmpweqnn  17107  symgextf1  19686  01eq0ringOLD  20833  nzerooringczr  21841  mamufacex  22766  mavmulsolcl  22921  chfacfscmulgsum  23233  chfacfpmmulgsum  23237  logbgcd1irr  27179  lgsqrmodndvds  27737  gausslemma2dlem0f  27745  gausslemma2dlem0i  27748  2lgs  27791  2lgsoddprm  27800  2sqreultlem  27831  2sqreunnltlem  27834  ltlesnd  28189  umgrnloop2  29781  uhgr2edg  29846  uvtx01vtx  30035  g0wlk0  30288  wlkreslem  30305  upgrwlkdvdelem  30379  uspgrn2crct  30454  wspn0  30570  2pthdlem1  30576  2pthon3v  30589  umgr2adedgspth  30594  umgrclwwlkge2  30639  lppthon  30799  1pthon2v  30811  frgrwopreglem4a  30968  frgrreg  31052  frgrregord13  31054  frgrogt3nreg  31055  nsnlplig  31140  nsnlpligALT  31141  gonarlem  36367  gonar  36368  goalrlem  36369  goalr  36370  bj-prmoore  38306  prproropf1olem4  48861  paireqne  48866  goldbachth  48905  lighneallem2  48964  lighneal  48969  requad1  48993  evenltle  49088  fppr2odd  49102  elclnbgrelnbgr  49196  vopnbgrelself  49226  dfnbgr6  49228  isubgr3stgrlem4  49340  isubgr3stgrlem7  49343  gpgvtxedg0  49434  gpgvtxedg1  49435  gpgedgiov  49436  gpgedg2ov  49437  gpgedg2iv  49438  gpgprismgr4cycllem7  49472  pgnioedg1  49479  pgnioedg2  49480  pgnioedg3  49481  pgnioedg4  49482  pgnioedg5  49483  pgnbgreunbgrlem1  49484  pgnbgreunbgrlem2lem1  49485  pgnbgreunbgrlem2lem2  49486  pgnbgreunbgrlem2lem3  49487  pgnbgreunbgrlem2  49488  pgnbgreunbgrlem4  49490  pgnbgreunbgrlem5lem1  49491  pgnbgreunbgrlem5lem2  49492  pgnbgreunbgrlem5  49494  lidldomn1  49601  ztprmneprm  49790  suppmptcfin  49819  linc1  49868  lindsrng01  49911  ldepspr  49916  zlmodzxznm  49940  rrx2plord2  50166  line2ylem  50194  line2xlem  50196  line2y  50198  inlinecirc02plem  50229