Theorem eqneqall 2941

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1534   ≠ wne 2930

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 2931

This theorem is referenced by:  nonconne  2942  ssprsseq  4824  prnebg  4854  preqsnd  4857  preq12nebg  4861  prel12g  4862  opthprneg  4863  3elpr2eq  4904  snopeqop  5504  propssopi  5506  opthhausdorff  5515  opthhausdorff0  5516  iunopeqop  5519  tpres  7210  elovmpt3imp  7675  bropopvvv  8096  bropfvvvvlem  8097  infsupprpr  9540  epnsym  9645  eldju2ndl  9960  eldju2ndr  9961  fin1a2lem10  10443  modfzo0difsn  13957  suppssfz  14008  hashrabsn1  14386  hash2pwpr  14490  hashle2pr  14491  hashge2el2difr  14495  cshwidxmod  14806  cshwidx0  14809  mod2eq1n2dvds  16344  nno  16379  prm2orodd  16687  prm23lt5  16811  dvdsprmpweqnn  16882  symgextf1  19415  01eq0ringOLD  20509  nzerooringczr  21466  mamufacex  22384  mavmulsolcl  22541  chfacfscmulgsum  22850  chfacfpmmulgsum  22854  logbgcd1irr  26819  lgsqrmodndvds  27379  gausslemma2dlem0f  27387  gausslemma2dlem0i  27390  2lgs  27433  2lgsoddprm  27442  2sqreultlem  27473  2sqreunnltlem  27476  sltlend  27798  umgrnloop2  29079  uhgr2edg  29141  uvtx01vtx  29330  g0wlk0  29586  wlkreslem  29603  upgrwlkdvdelem  29670  uspgrn2crct  29739  wspn0  29855  2pthdlem1  29861  2pthon3v  29874  umgr2adedgspth  29879  umgrclwwlkge2  29921  lppthon  30081  1pthon2v  30083  frgrwopreglem4a  30240  frgrreg  30324  frgrregord13  30326  frgrogt3nreg  30327  nsnlplig  30411  nsnlpligALT  30412  gonarlem  35235  gonar  35236  goalrlem  35237  goalr  35238  bj-prmoore  36835  prproropf1olem4  47114  paireqne  47119  goldbachth  47155  lighneallem2  47214  lighneal  47219  requad1  47230  evenltle  47325  fppr2odd  47339  vopnbgrelself  47458  dfnbgr6  47460  lidldomn1  47644  ztprmneprm  47762  suppmptcfin  47794  linc1  47844  lindsrng01  47887  ldepspr  47892  zlmodzxznm  47916  rrx2xpref1o  48142  rrx2plord2  48146  line2ylem  48175  line2xlem  48177  line2y  48179  inlinecirc02plem  48210