Theorem eqneqall 2937

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

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

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 2927

This theorem is referenced by:  nonconne  2938  ssprsseq  4792  prnebg  4823  preqsnd  4826  preq12nebg  4830  prel12g  4831  opthprneg  4832  3elpr2eq  4873  snopeqop  5469  propssopi  5471  opthhausdorff  5480  opthhausdorff0  5481  iunopeqop  5484  tpres  7178  f1ounsn  7250  fvf1pr  7285  elovmpt3imp  7649  resf1extb  7913  bropopvvv  8072  bropfvvvvlem  8073  infsupprpr  9464  epnsym  9569  eldju2ndl  9884  eldju2ndr  9885  fin1a2lem10  10369  fvf1tp  13758  modfzo0difsn  13915  suppssfz  13966  hashrabsn1  14346  hash2pwpr  14448  hashle2pr  14449  hashge2el2difr  14453  cshwidxmod  14775  cshwidx0  14778  mod2eq1n2dvds  16324  nno  16359  prm2orodd  16668  prm23lt5  16792  dvdsprmpweqnn  16863  symgextf1  19358  01eq0ringOLD  20447  nzerooringczr  21397  mamufacex  22290  mavmulsolcl  22445  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  logbgcd1irr  26711  lgsqrmodndvds  27271  gausslemma2dlem0f  27279  gausslemma2dlem0i  27282  2lgs  27325  2lgsoddprm  27334  2sqreultlem  27365  2sqreunnltlem  27368  sltlend  27690  umgrnloop2  29080  uhgr2edg  29142  uvtx01vtx  29331  g0wlk0  29587  wlkreslem  29604  upgrwlkdvdelem  29673  uspgrn2crct  29745  wspn0  29861  2pthdlem1  29867  2pthon3v  29880  umgr2adedgspth  29885  umgrclwwlkge2  29927  lppthon  30087  1pthon2v  30089  frgrwopreglem4a  30246  frgrreg  30330  frgrregord13  30332  frgrogt3nreg  30333  nsnlplig  30417  nsnlpligALT  30418  gonarlem  35388  gonar  35389  goalrlem  35390  goalr  35391  bj-prmoore  37110  prproropf1olem4  47511  paireqne  47516  goldbachth  47552  lighneallem2  47611  lighneal  47616  requad1  47627  evenltle  47722  fppr2odd  47736  elclnbgrelnbgr  47830  vopnbgrelself  47859  dfnbgr6  47861  isubgr3stgrlem4  47972  isubgr3stgrlem7  47975  gpgvtxedg0  48058  gpgvtxedg1  48059  gpgedgiov  48060  gpgedg2ov  48061  gpgedg2iv  48062  gpgprismgr4cycllem7  48095  pgnioedg1  48102  pgnioedg2  48103  pgnioedg3  48104  pgnioedg4  48105  pgnioedg5  48106  pgnbgreunbgrlem1  48107  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  pgnbgreunbgrlem2  48111  pgnbgreunbgrlem4  48113  pgnbgreunbgrlem5lem1  48114  pgnbgreunbgrlem5lem2  48115  pgnbgreunbgrlem5  48117  lidldomn1  48223  ztprmneprm  48339  suppmptcfin  48368  linc1  48418  lindsrng01  48461  ldepspr  48466  zlmodzxznm  48490  rrx2xpref1o  48711  rrx2plord2  48715  line2ylem  48744  line2xlem  48746  line2y  48748  inlinecirc02plem  48779