Theorem eqneqall 2940

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2929

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 2930

This theorem is referenced by:  nonconne  2941  ssprsseq  4778  prnebg  4809  preqsnd  4812  preq12nebg  4816  prel12g  4817  opthprneg  4818  3elpr2eq  4859  snopeqop  5451  propssopi  5453  opthhausdorff  5462  opthhausdorff0  5463  iunopeqop  5466  tpres  7144  f1ounsn  7215  fvf1pr  7250  elovmpt3imp  7612  resf1extb  7873  bropopvvv  8029  bropfvvvvlem  8030  infsupprpr  9401  epnsym  9510  eldju2ndl  9828  eldju2ndr  9829  fin1a2lem10  10311  fvf1tp  13700  modfzo0difsn  13857  suppssfz  13908  hashrabsn1  14288  hash2pwpr  14390  hashle2pr  14391  hashge2el2difr  14395  cshwidxmod  14717  cshwidx0  14720  mod2eq1n2dvds  16265  nno  16300  prm2orodd  16609  prm23lt5  16733  dvdsprmpweqnn  16804  symgextf1  19341  01eq0ringOLD  20455  nzerooringczr  21426  mamufacex  22331  mavmulsolcl  22486  chfacfscmulgsum  22795  chfacfpmmulgsum  22799  logbgcd1irr  26751  lgsqrmodndvds  27311  gausslemma2dlem0f  27319  gausslemma2dlem0i  27322  2lgs  27365  2lgsoddprm  27374  2sqreultlem  27405  2sqreunnltlem  27408  sltlend  27730  umgrnloop2  29145  uhgr2edg  29207  uvtx01vtx  29396  g0wlk0  29650  wlkreslem  29667  upgrwlkdvdelem  29735  uspgrn2crct  29807  wspn0  29923  2pthdlem1  29929  2pthon3v  29942  umgr2adedgspth  29947  umgrclwwlkge2  29992  lppthon  30152  1pthon2v  30154  frgrwopreglem4a  30311  frgrreg  30395  frgrregord13  30397  frgrogt3nreg  30398  nsnlplig  30482  nsnlpligALT  30483  gonarlem  35510  gonar  35511  goalrlem  35512  goalr  35513  bj-prmoore  37232  prproropf1olem4  47668  paireqne  47673  goldbachth  47709  lighneallem2  47768  lighneal  47773  requad1  47784  evenltle  47879  fppr2odd  47893  elclnbgrelnbgr  47987  vopnbgrelself  48017  dfnbgr6  48019  isubgr3stgrlem4  48131  isubgr3stgrlem7  48134  gpgvtxedg0  48225  gpgvtxedg1  48226  gpgedgiov  48227  gpgedg2ov  48228  gpgedg2iv  48229  gpgprismgr4cycllem7  48263  pgnioedg1  48270  pgnioedg2  48271  pgnioedg3  48272  pgnioedg4  48273  pgnioedg5  48274  pgnbgreunbgrlem1  48275  pgnbgreunbgrlem2lem1  48276  pgnbgreunbgrlem2lem2  48277  pgnbgreunbgrlem2lem3  48278  pgnbgreunbgrlem2  48279  pgnbgreunbgrlem4  48281  pgnbgreunbgrlem5lem1  48282  pgnbgreunbgrlem5lem2  48283  pgnbgreunbgrlem5  48285  lidldomn1  48393  ztprmneprm  48509  suppmptcfin  48538  linc1  48587  lindsrng01  48630  ldepspr  48635  zlmodzxznm  48659  rrx2xpref1o  48880  rrx2plord2  48884  line2ylem  48913  line2xlem  48915  line2y  48917  inlinecirc02plem  48948