Theorem eqneqall 2951

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

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

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 2941

This theorem is referenced by:  nonconne  2952  ssprsseq  4825  prnebg  4856  preqsnd  4859  preq12nebg  4863  prel12g  4864  opthprneg  4865  3elpr2eq  4906  snopeqop  5511  propssopi  5513  opthhausdorff  5522  opthhausdorff0  5523  iunopeqop  5526  tpres  7221  f1ounsn  7292  fvf1pr  7327  elovmpt3imp  7690  resf1extb  7956  bropopvvv  8115  bropfvvvvlem  8116  infsupprpr  9544  epnsym  9649  eldju2ndl  9964  eldju2ndr  9965  fin1a2lem10  10449  fvf1tp  13829  modfzo0difsn  13984  suppssfz  14035  hashrabsn1  14413  hash2pwpr  14515  hashle2pr  14516  hashge2el2difr  14520  cshwidxmod  14841  cshwidx0  14844  mod2eq1n2dvds  16384  nno  16419  prm2orodd  16728  prm23lt5  16852  dvdsprmpweqnn  16923  symgextf1  19439  01eq0ringOLD  20531  nzerooringczr  21491  mamufacex  22400  mavmulsolcl  22557  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  logbgcd1irr  26837  lgsqrmodndvds  27397  gausslemma2dlem0f  27405  gausslemma2dlem0i  27408  2lgs  27451  2lgsoddprm  27460  2sqreultlem  27491  2sqreunnltlem  27494  sltlend  27816  umgrnloop2  29163  uhgr2edg  29225  uvtx01vtx  29414  g0wlk0  29670  wlkreslem  29687  upgrwlkdvdelem  29756  uspgrn2crct  29828  wspn0  29944  2pthdlem1  29950  2pthon3v  29963  umgr2adedgspth  29968  umgrclwwlkge2  30010  lppthon  30170  1pthon2v  30172  frgrwopreglem4a  30329  frgrreg  30413  frgrregord13  30415  frgrogt3nreg  30416  nsnlplig  30500  nsnlpligALT  30501  gonarlem  35399  gonar  35400  goalrlem  35401  goalr  35402  bj-prmoore  37116  prproropf1olem4  47493  paireqne  47498  goldbachth  47534  lighneallem2  47593  lighneal  47598  requad1  47609  evenltle  47704  fppr2odd  47718  elclnbgrelnbgr  47812  vopnbgrelself  47841  dfnbgr6  47843  isubgr3stgrlem4  47936  isubgr3stgrlem7  47939  gpgvtxedg0  48021  gpgvtxedg1  48022  lidldomn1  48147  ztprmneprm  48263  suppmptcfin  48292  linc1  48342  lindsrng01  48385  ldepspr  48390  zlmodzxznm  48414  rrx2xpref1o  48639  rrx2plord2  48643  line2ylem  48672  line2xlem  48674  line2y  48676  inlinecirc02plem  48707