Theorem eqneqall 2952

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2941

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 2942

This theorem is referenced by:  nonconne  2953  ssprsseq  4829  prnebg  4857  preqsnd  4860  preq12nebg  4864  prel12g  4865  opthprneg  4866  3elpr2eq  4908  snopeqop  5507  propssopi  5509  opthhausdorff  5518  opthhausdorff0  5519  iunopeqop  5522  tpres  7202  elovmpt3imp  7663  bropopvvv  8076  bropfvvvvlem  8077  infsupprpr  9499  epnsym  9604  eldju2ndl  9919  eldju2ndr  9920  fin1a2lem10  10404  modfzo0difsn  13908  suppssfz  13959  hashrabsn1  14334  hash2pwpr  14437  hashle2pr  14438  hashge2el2difr  14442  cshwidxmod  14753  cshwidx0  14756  mod2eq1n2dvds  16290  nno  16325  prm2orodd  16628  prm23lt5  16747  dvdsprmpweqnn  16818  symgextf1  19289  01eq0ringOLD  20306  mamufacex  21891  mavmulsolcl  22053  chfacfscmulgsum  22362  chfacfpmmulgsum  22366  logbgcd1irr  26299  lgsqrmodndvds  26856  gausslemma2dlem0f  26864  gausslemma2dlem0i  26867  2lgs  26910  2lgsoddprm  26919  2sqreultlem  26950  2sqreunnltlem  26953  umgrnloop2  28406  uhgr2edg  28465  uvtx01vtx  28654  g0wlk0  28909  wlkreslem  28926  upgrwlkdvdelem  28993  uspgrn2crct  29062  wspn0  29178  2pthdlem1  29184  2pthon3v  29197  umgr2adedgspth  29202  umgrclwwlkge2  29244  lppthon  29404  1pthon2v  29406  frgrwopreglem4a  29563  frgrreg  29647  frgrregord13  29649  frgrogt3nreg  29650  nsnlplig  29734  nsnlpligALT  29735  gonarlem  34385  gonar  34386  goalrlem  34387  goalr  34388  bj-prmoore  35996  prproropf1olem4  46174  paireqne  46179  goldbachth  46215  lighneallem2  46274  lighneal  46279  requad1  46290  evenltle  46385  fppr2odd  46399  lidldomn1  46823  nzerooringczr  46970  ztprmneprm  47023  suppmptcfin  47055  linc1  47106  lindsrng01  47149  ldepspr  47154  zlmodzxznm  47178  rrx2xpref1o  47404  rrx2plord2  47408  line2ylem  47437  line2xlem  47439  line2y  47441  inlinecirc02plem  47472