Theorem eqneqall 2936

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

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

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 2926

This theorem is referenced by:  nonconne  2937  ssprsseq  4789  prnebg  4820  preqsnd  4823  preq12nebg  4827  prel12g  4828  opthprneg  4829  3elpr2eq  4870  snopeqop  5466  propssopi  5468  opthhausdorff  5477  opthhausdorff0  5478  iunopeqop  5481  tpres  7175  f1ounsn  7247  fvf1pr  7282  elovmpt3imp  7646  resf1extb  7910  bropopvvv  8069  bropfvvvvlem  8070  infsupprpr  9457  epnsym  9562  eldju2ndl  9877  eldju2ndr  9878  fin1a2lem10  10362  fvf1tp  13751  modfzo0difsn  13908  suppssfz  13959  hashrabsn1  14339  hash2pwpr  14441  hashle2pr  14442  hashge2el2difr  14446  cshwidxmod  14768  cshwidx0  14771  mod2eq1n2dvds  16317  nno  16352  prm2orodd  16661  prm23lt5  16785  dvdsprmpweqnn  16856  symgextf1  19351  01eq0ringOLD  20440  nzerooringczr  21390  mamufacex  22283  mavmulsolcl  22438  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  logbgcd1irr  26704  lgsqrmodndvds  27264  gausslemma2dlem0f  27272  gausslemma2dlem0i  27275  2lgs  27318  2lgsoddprm  27327  2sqreultlem  27358  2sqreunnltlem  27361  sltlend  27683  umgrnloop2  29073  uhgr2edg  29135  uvtx01vtx  29324  g0wlk0  29580  wlkreslem  29597  upgrwlkdvdelem  29666  uspgrn2crct  29738  wspn0  29854  2pthdlem1  29860  2pthon3v  29873  umgr2adedgspth  29878  umgrclwwlkge2  29920  lppthon  30080  1pthon2v  30082  frgrwopreglem4a  30239  frgrreg  30323  frgrregord13  30325  frgrogt3nreg  30326  nsnlplig  30410  nsnlpligALT  30411  gonarlem  35381  gonar  35382  goalrlem  35383  goalr  35384  bj-prmoore  37103  prproropf1olem4  47507  paireqne  47512  goldbachth  47548  lighneallem2  47607  lighneal  47612  requad1  47623  evenltle  47718  fppr2odd  47732  elclnbgrelnbgr  47826  vopnbgrelself  47855  dfnbgr6  47857  isubgr3stgrlem4  47968  isubgr3stgrlem7  47971  gpgvtxedg0  48054  gpgvtxedg1  48055  gpgedgiov  48056  gpgedg2ov  48057  gpgedg2iv  48058  gpgprismgr4cycllem7  48091  pgnioedg1  48098  pgnioedg2  48099  pgnioedg3  48100  pgnioedg4  48101  pgnioedg5  48102  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  pgnbgreunbgrlem2  48107  pgnbgreunbgrlem4  48109  pgnbgreunbgrlem5lem1  48110  pgnbgreunbgrlem5lem2  48111  pgnbgreunbgrlem5  48113  lidldomn1  48219  ztprmneprm  48335  suppmptcfin  48364  linc1  48414  lindsrng01  48457  ldepspr  48462  zlmodzxznm  48486  rrx2xpref1o  48707  rrx2plord2  48711  line2ylem  48740  line2xlem  48742  line2y  48744  inlinecirc02plem  48775