Theorem eqneqall 2975

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1567   ≠ wne 2964

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 2965

This theorem is referenced by:  nonconne  2976  ssprsseq  4792  prnebg  4822  preqsnd  4825  preq12nebg  4829  prel12g  4830  opthprneg  4831  3elpr2eq  4872  snopeqop  5487  propssopi  5489  opthhausdorff  5498  opthhausdorff0  5499  iunopeqop  5502  iunopeqopOLD  5503  tpres  7197  f1ounsn  7268  fvf1pr  7303  elovmpt3imp  7665  resf1extb  7927  bropopvvv  8081  bropfvvvvlem  8082  infsupprpr  9462  epnsym  9574  eldju2ndl  9906  eldju2ndr  9907  fin1a2lem10  10389  fvf1tp  13818  modfzo0difsn  13975  suppssfz  14026  hashrabsn1  14406  hash2pwpr  14509  hashle2pr  14510  hashge2el2difr  14514  cshwidxmod  14836  cshwidx0  14839  mod2eq1n2dvds  16401  nno  16436  prm2orodd  16745  prm23lt5  16870  dvdsprmpweqnn  16941  symgextf1  19487  01eq0ringOLD  20611  nzerooringczr  21595  mamufacex  22518  mavmulsolcl  22673  chfacfscmulgsum  22982  chfacfpmmulgsum  22986  logbgcd1irr  26921  lgsqrmodndvds  27479  gausslemma2dlem0f  27487  gausslemma2dlem0i  27490  2lgs  27533  2lgsoddprm  27542  2sqreultlem  27573  2sqreunnltlem  27576  ltlesnd  27901  umgrnloop2  29433  uhgr2edg  29495  uvtx01vtx  29684  g0wlk0  29937  wlkreslem  29954  upgrwlkdvdelem  30022  uspgrn2crct  30094  wspn0  30210  2pthdlem1  30216  2pthon3v  30229  umgr2adedgspth  30234  umgrclwwlkge2  30279  lppthon  30439  1pthon2v  30441  frgrwopreglem4a  30598  frgrreg  30682  frgrregord13  30684  frgrogt3nreg  30685  nsnlplig  30770  nsnlpligALT  30771  gonarlem  35781  gonar  35782  goalrlem  35783  goalr  35784  bj-prmoore  37640  prproropf1olem4  48139  paireqne  48144  goldbachth  48183  lighneallem2  48242  lighneal  48247  requad1  48271  evenltle  48366  fppr2odd  48380  elclnbgrelnbgr  48474  vopnbgrelself  48504  dfnbgr6  48506  isubgr3stgrlem4  48618  isubgr3stgrlem7  48621  gpgvtxedg0  48712  gpgvtxedg1  48713  gpgedgiov  48714  gpgedg2ov  48715  gpgedg2iv  48716  gpgprismgr4cycllem7  48750  pgnioedg1  48757  pgnioedg2  48758  pgnioedg3  48759  pgnioedg4  48760  pgnioedg5  48761  pgnbgreunbgrlem1  48762  pgnbgreunbgrlem2lem1  48763  pgnbgreunbgrlem2lem2  48764  pgnbgreunbgrlem2lem3  48765  pgnbgreunbgrlem2  48766  pgnbgreunbgrlem4  48768  pgnbgreunbgrlem5lem1  48769  pgnbgreunbgrlem5lem2  48770  pgnbgreunbgrlem5  48772  lidldomn1  48880  ztprmneprm  49007  suppmptcfin  49036  linc1  49085  lindsrng01  49128  ldepspr  49133  zlmodzxznm  49157  rrx2xpref1o  49378  rrx2plord2  49382  line2ylem  49411  line2xlem  49413  line2y  49415  inlinecirc02plem  49446