Theorem eqneqall 2936

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

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

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 2926

This theorem is referenced by:  nonconne  2937  ssprsseq  4785  prnebg  4816  preqsnd  4819  preq12nebg  4823  prel12g  4824  opthprneg  4825  3elpr2eq  4866  snopeqop  5461  propssopi  5463  opthhausdorff  5472  opthhausdorff0  5473  iunopeqop  5476  tpres  7157  f1ounsn  7229  fvf1pr  7264  elovmpt3imp  7626  resf1extb  7890  bropopvvv  8046  bropfvvvvlem  8047  infsupprpr  9433  epnsym  9538  eldju2ndl  9853  eldju2ndr  9854  fin1a2lem10  10338  fvf1tp  13727  modfzo0difsn  13884  suppssfz  13935  hashrabsn1  14315  hash2pwpr  14417  hashle2pr  14418  hashge2el2difr  14422  cshwidxmod  14744  cshwidx0  14747  mod2eq1n2dvds  16293  nno  16328  prm2orodd  16637  prm23lt5  16761  dvdsprmpweqnn  16832  symgextf1  19327  01eq0ringOLD  20416  nzerooringczr  21366  mamufacex  22259  mavmulsolcl  22414  chfacfscmulgsum  22723  chfacfpmmulgsum  22727  logbgcd1irr  26680  lgsqrmodndvds  27240  gausslemma2dlem0f  27248  gausslemma2dlem0i  27251  2lgs  27294  2lgsoddprm  27303  2sqreultlem  27334  2sqreunnltlem  27337  sltlend  27659  umgrnloop2  29049  uhgr2edg  29111  uvtx01vtx  29300  g0wlk0  29554  wlkreslem  29571  upgrwlkdvdelem  29639  uspgrn2crct  29711  wspn0  29827  2pthdlem1  29833  2pthon3v  29846  umgr2adedgspth  29851  umgrclwwlkge2  29893  lppthon  30053  1pthon2v  30055  frgrwopreglem4a  30212  frgrreg  30296  frgrregord13  30298  frgrogt3nreg  30299  nsnlplig  30383  nsnlpligALT  30384  gonarlem  35354  gonar  35355  goalrlem  35356  goalr  35357  bj-prmoore  37076  prproropf1olem4  47480  paireqne  47485  goldbachth  47521  lighneallem2  47580  lighneal  47585  requad1  47596  evenltle  47691  fppr2odd  47705  elclnbgrelnbgr  47799  vopnbgrelself  47828  dfnbgr6  47830  isubgr3stgrlem4  47941  isubgr3stgrlem7  47944  gpgvtxedg0  48027  gpgvtxedg1  48028  gpgedgiov  48029  gpgedg2ov  48030  gpgedg2iv  48031  gpgprismgr4cycllem7  48064  pgnioedg1  48071  pgnioedg2  48072  pgnioedg3  48073  pgnioedg4  48074  pgnioedg5  48075  pgnbgreunbgrlem1  48076  pgnbgreunbgrlem2lem1  48077  pgnbgreunbgrlem2lem2  48078  pgnbgreunbgrlem2lem3  48079  pgnbgreunbgrlem2  48080  pgnbgreunbgrlem4  48082  pgnbgreunbgrlem5lem1  48083  pgnbgreunbgrlem5lem2  48084  pgnbgreunbgrlem5  48086  lidldomn1  48192  ztprmneprm  48308  suppmptcfin  48337  linc1  48387  lindsrng01  48430  ldepspr  48435  zlmodzxznm  48459  rrx2xpref1o  48680  rrx2plord2  48684  line2ylem  48713  line2xlem  48715  line2y  48717  inlinecirc02plem  48748