Theorem eqneqall 2969

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2958

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 210  df-ne 2959

This theorem is referenced by:  nonconne  2970  ssprsseq  4791  prnebg  4821  preqsnd  4824  preq12nebg  4828  prel12g  4829  opthprneg  4830  3elpr2eq  4871  snopeqop  5489  propssopi  5491  opthhausdorff  5500  opthhausdorff0  5501  iunopeqop  5504  iunopeqopOLD  5505  tpres  7199  f1ounsn  7270  fvf1pr  7305  elovmpt3imp  7667  resf1extb  7927  bropopvvv  8081  bropfvvvvlem  8082  infsupprpr  9462  epnsym  9574  eldju2ndl  9906  eldju2ndr  9907  fin1a2lem10  10388  fvf1tp  13818  modfzo0difsn  13975  suppssfz  14026  hashrabsn1  14406  hash2pwpr  14509  hashle2pr  14510  hashge2el2difr  14514  cshwidxmod  14836  cshwidx0  14839  mod2eq1n2dvds  16400  nno  16435  prm2orodd  16744  prm23lt5  16869  dvdsprmpweqnn  16940  symgextf1  19486  01eq0ringOLD  20629  nzerooringczr  21630  mamufacex  22553  mavmulsolcl  22708  chfacfscmulgsum  23017  chfacfpmmulgsum  23021  logbgcd1irr  26959  lgsqrmodndvds  27517  gausslemma2dlem0f  27525  gausslemma2dlem0i  27528  2lgs  27571  2lgsoddprm  27580  2sqreultlem  27611  2sqreunnltlem  27614  ltlesnd  27939  umgrnloop2  29496  uhgr2edg  29558  uvtx01vtx  29747  g0wlk0  30000  wlkreslem  30017  upgrwlkdvdelem  30085  uspgrn2crct  30157  wspn0  30273  2pthdlem1  30279  2pthon3v  30292  umgr2adedgspth  30297  umgrclwwlkge2  30342  lppthon  30502  1pthon2v  30504  frgrwopreglem4a  30661  frgrreg  30745  frgrregord13  30747  frgrogt3nreg  30748  nsnlplig  30833  nsnlpligALT  30834  gonarlem  35886  gonar  35887  goalrlem  35888  goalr  35889  bj-prmoore  37757  prproropf1olem4  48255  paireqne  48260  goldbachth  48299  lighneallem2  48358  lighneal  48363  requad1  48387  evenltle  48482  fppr2odd  48496  elclnbgrelnbgr  48590  vopnbgrelself  48620  dfnbgr6  48622  isubgr3stgrlem4  48734  isubgr3stgrlem7  48737  gpgvtxedg0  48828  gpgvtxedg1  48829  gpgedgiov  48830  gpgedg2ov  48831  gpgedg2iv  48832  gpgprismgr4cycllem7  48866  pgnioedg1  48873  pgnioedg2  48874  pgnioedg3  48875  pgnioedg4  48876  pgnioedg5  48877  pgnbgreunbgrlem1  48878  pgnbgreunbgrlem2lem1  48879  pgnbgreunbgrlem2lem2  48880  pgnbgreunbgrlem2lem3  48881  pgnbgreunbgrlem2  48882  pgnbgreunbgrlem4  48884  pgnbgreunbgrlem5lem1  48885  pgnbgreunbgrlem5lem2  48886  pgnbgreunbgrlem5  48888  lidldomn1  48996  ztprmneprm  49127  suppmptcfin  49156  linc1  49205  lindsrng01  49248  ldepspr  49253  zlmodzxznm  49277  rrx2xpref1o  49498  rrx2plord2  49502  line2ylem  49531  line2xlem  49533  line2y  49535  inlinecirc02plem  49566