Theorem eqneqall 2951

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

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

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 206  df-ne 2941

This theorem is referenced by:  nonconne  2952  ssprsseq  4769  prnebg  4797  preqsnd  4800  preq12nebg  4804  prel12g  4805  opthprneg  4806  3elpr2eq  4848  snopeqop  5438  propssopi  5440  opthhausdorff  5449  opthhausdorff0  5450  iunopeqop  5453  tpres  7115  elovmpt3imp  7567  bropopvvv  7976  bropfvvvvlem  7977  infsupprpr  9339  epnsym  9444  eldju2ndl  9759  eldju2ndr  9760  fin1a2lem10  10244  modfzo0difsn  13742  suppssfz  13793  hashrabsn1  14167  hash2pwpr  14268  hashle2pr  14269  hashge2el2difr  14273  cshwidxmod  14592  cshwidx0  14595  mod2eq1n2dvds  16132  nno  16167  prm2orodd  16470  prm23lt5  16589  dvdsprmpweqnn  16660  symgextf1  19102  01eq0ring  20623  mamufacex  21618  mavmulsolcl  21780  chfacfscmulgsum  22089  chfacfpmmulgsum  22093  logbgcd1irr  26024  lgsqrmodndvds  26581  gausslemma2dlem0f  26589  gausslemma2dlem0i  26592  2lgs  26635  2lgsoddprm  26644  2sqreultlem  26675  2sqreunnltlem  26678  umgrnloop2  27649  uhgr2edg  27708  uvtx01vtx  27897  g0wlk0  28152  wlkreslem  28169  upgrwlkdvdelem  28236  uspgrn2crct  28305  wspn0  28421  2pthdlem1  28427  2pthon3v  28440  umgr2adedgspth  28445  umgrclwwlkge2  28487  lppthon  28647  1pthon2v  28649  frgrwopreglem4a  28806  frgrreg  28890  frgrregord13  28892  frgrogt3nreg  28893  nsnlplig  28975  nsnlpligALT  28976  gonarlem  33491  gonar  33492  goalrlem  33493  goalr  33494  bj-prmoore  35363  prproropf1olem4  45228  paireqne  45233  goldbachth  45269  lighneallem2  45328  lighneal  45333  requad1  45344  evenltle  45439  fppr2odd  45453  lidldomn1  45749  nzerooringczr  45900  ztprmneprm  45953  suppmptcfin  45985  linc1  46036  lindsrng01  46079  ldepspr  46084  zlmodzxznm  46108  rrx2xpref1o  46334  rrx2plord2  46338  line2ylem  46367  line2xlem  46369  line2y  46371  inlinecirc02plem  46402