Theorem eqneqall 2945

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ≠ wne 2934

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 208  df-ne 2935

This theorem is referenced by:  nonconne  2946  ssprsseq  4756  prnebg  4787  preqsnd  4790  preq12nebg  4794  prel12g  4795  opthprneg  4796  3elpr2eq  4837  snopeqop  5447  propssopi  5449  opthhausdorff  5458  opthhausdorff0  5459  iunopeqop  5462  iunopeqopOLD  5463  tpres  7145  f1ounsn  7216  fvf1pr  7251  elovmpt3imp  7613  resf1extb  7874  bropopvvv  8029  bropfvvvvlem  8030  infsupprpr  9409  epnsym  9521  eldju2ndl  9839  eldju2ndr  9840  fin1a2lem10  10322  fvf1tp  13739  modfzo0difsn  13896  suppssfz  13947  hashrabsn1  14327  hash2pwpr  14429  hashle2pr  14430  hashge2el2difr  14434  cshwidxmod  14756  cshwidx0  14759  mod2eq1n2dvds  16307  nno  16342  prm2orodd  16651  prm23lt5  16776  dvdsprmpweqnn  16847  symgextf1  19387  01eq0ringOLD  20503  nzerooringczr  21455  mamufacex  22379  mavmulsolcl  22534  chfacfscmulgsum  22843  chfacfpmmulgsum  22847  logbgcd1irr  26776  lgsqrmodndvds  27334  gausslemma2dlem0f  27342  gausslemma2dlem0i  27345  2lgs  27388  2lgsoddprm  27397  2sqreultlem  27428  2sqreunnltlem  27431  ltlesnd  27757  umgrnloop2  29233  uhgr2edg  29295  uvtx01vtx  29484  g0wlk0  29737  wlkreslem  29754  upgrwlkdvdelem  29822  uspgrn2crct  29894  wspn0  30010  2pthdlem1  30016  2pthon3v  30029  umgr2adedgspth  30034  umgrclwwlkge2  30079  lppthon  30239  1pthon2v  30241  frgrwopreglem4a  30398  frgrreg  30482  frgrregord13  30484  frgrogt3nreg  30485  nsnlplig  30570  nsnlpligALT  30571  gonarlem  35622  gonar  35623  goalrlem  35624  goalr  35625  bj-prmoore  37473  prproropf1olem4  47981  paireqne  47986  goldbachth  48025  lighneallem2  48084  lighneal  48089  requad1  48113  evenltle  48208  fppr2odd  48222  elclnbgrelnbgr  48316  vopnbgrelself  48346  dfnbgr6  48348  isubgr3stgrlem4  48460  isubgr3stgrlem7  48463  gpgvtxedg0  48554  gpgvtxedg1  48555  gpgedgiov  48556  gpgedg2ov  48557  gpgedg2iv  48558  gpgprismgr4cycllem7  48592  pgnioedg1  48599  pgnioedg2  48600  pgnioedg3  48601  pgnioedg4  48602  pgnioedg5  48603  pgnbgreunbgrlem1  48604  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  pgnbgreunbgrlem2  48608  pgnbgreunbgrlem4  48610  pgnbgreunbgrlem5lem1  48611  pgnbgreunbgrlem5lem2  48612  pgnbgreunbgrlem5  48614  lidldomn1  48722  ztprmneprm  48838  suppmptcfin  48867  linc1  48916  lindsrng01  48959  ldepspr  48964  zlmodzxznm  48988  rrx2xpref1o  49209  rrx2plord2  49213  line2ylem  49242  line2xlem  49244  line2y  49246  inlinecirc02plem  49277