Theorem eqneqall 2949

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2938

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 2939

This theorem is referenced by:  nonconne  2950  ssprsseq  4830  prnebg  4861  preqsnd  4864  preq12nebg  4868  prel12g  4869  opthprneg  4870  3elpr2eq  4911  snopeqop  5516  propssopi  5518  opthhausdorff  5527  opthhausdorff0  5528  iunopeqop  5531  tpres  7221  f1ounsn  7292  fvf1pr  7327  elovmpt3imp  7690  bropopvvv  8114  bropfvvvvlem  8115  infsupprpr  9542  epnsym  9647  eldju2ndl  9962  eldju2ndr  9963  fin1a2lem10  10447  fvf1tp  13826  modfzo0difsn  13981  suppssfz  14032  hashrabsn1  14410  hash2pwpr  14512  hashle2pr  14513  hashge2el2difr  14517  cshwidxmod  14838  cshwidx0  14841  mod2eq1n2dvds  16381  nno  16416  prm2orodd  16725  prm23lt5  16848  dvdsprmpweqnn  16919  symgextf1  19454  01eq0ringOLD  20548  nzerooringczr  21509  mamufacex  22416  mavmulsolcl  22573  chfacfscmulgsum  22882  chfacfpmmulgsum  22886  logbgcd1irr  26852  lgsqrmodndvds  27412  gausslemma2dlem0f  27420  gausslemma2dlem0i  27423  2lgs  27466  2lgsoddprm  27475  2sqreultlem  27506  2sqreunnltlem  27509  sltlend  27831  umgrnloop2  29178  uhgr2edg  29240  uvtx01vtx  29429  g0wlk0  29685  wlkreslem  29702  upgrwlkdvdelem  29769  uspgrn2crct  29838  wspn0  29954  2pthdlem1  29960  2pthon3v  29973  umgr2adedgspth  29978  umgrclwwlkge2  30020  lppthon  30180  1pthon2v  30182  frgrwopreglem4a  30339  frgrreg  30423  frgrregord13  30425  frgrogt3nreg  30426  nsnlplig  30510  nsnlpligALT  30511  gonarlem  35379  gonar  35380  goalrlem  35381  goalr  35382  bj-prmoore  37098  prproropf1olem4  47431  paireqne  47436  goldbachth  47472  lighneallem2  47531  lighneal  47536  requad1  47547  evenltle  47642  fppr2odd  47656  elclnbgrelnbgr  47750  vopnbgrelself  47779  dfnbgr6  47781  isubgr3stgrlem4  47872  isubgr3stgrlem7  47875  gpgvtxedg0  47956  gpgvtxedg1  47957  lidldomn1  48075  ztprmneprm  48192  suppmptcfin  48221  linc1  48271  lindsrng01  48314  ldepspr  48319  zlmodzxznm  48343  rrx2xpref1o  48568  rrx2plord2  48572  line2ylem  48601  line2xlem  48603  line2y  48605  inlinecirc02plem  48636