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 241	1 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ 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 206  df-ne 2939

This theorem is referenced by:  nonconne  2950  ssprsseq  4827  prnebg  4855  preqsnd  4858  preq12nebg  4862  prel12g  4863  opthprneg  4864  3elpr2eq  4906  snopeqop  5505  propssopi  5507  opthhausdorff  5516  opthhausdorff0  5517  iunopeqop  5520  tpres  7203  elovmpt3imp  7665  bropopvvv  8078  bropfvvvvlem  8079  infsupprpr  9501  epnsym  9606  eldju2ndl  9921  eldju2ndr  9922  fin1a2lem10  10406  modfzo0difsn  13912  suppssfz  13963  hashrabsn1  14338  hash2pwpr  14441  hashle2pr  14442  hashge2el2difr  14446  cshwidxmod  14757  cshwidx0  14760  mod2eq1n2dvds  16294  nno  16329  prm2orodd  16632  prm23lt5  16751  dvdsprmpweqnn  16822  symgextf1  19330  01eq0ringOLD  20420  mamufacex  22111  mavmulsolcl  22273  chfacfscmulgsum  22582  chfacfpmmulgsum  22586  logbgcd1irr  26535  lgsqrmodndvds  27092  gausslemma2dlem0f  27100  gausslemma2dlem0i  27103  2lgs  27146  2lgsoddprm  27155  2sqreultlem  27186  2sqreunnltlem  27189  umgrnloop2  28673  uhgr2edg  28732  uvtx01vtx  28921  g0wlk0  29176  wlkreslem  29193  upgrwlkdvdelem  29260  uspgrn2crct  29329  wspn0  29445  2pthdlem1  29451  2pthon3v  29464  umgr2adedgspth  29469  umgrclwwlkge2  29511  lppthon  29671  1pthon2v  29673  frgrwopreglem4a  29830  frgrreg  29914  frgrregord13  29916  frgrogt3nreg  29917  nsnlplig  30001  nsnlpligALT  30002  gonarlem  34683  gonar  34684  goalrlem  34685  goalr  34686  bj-prmoore  36299  prproropf1olem4  46472  paireqne  46477  goldbachth  46513  lighneallem2  46572  lighneal  46577  requad1  46588  evenltle  46683  fppr2odd  46697  lidldomn1  46911  nzerooringczr  47058  ztprmneprm  47111  suppmptcfin  47143  linc1  47193  lindsrng01  47236  ldepspr  47241  zlmodzxznm  47265  rrx2xpref1o  47491  rrx2plord2  47495  line2ylem  47524  line2xlem  47526  line2y  47528  inlinecirc02plem  47559