Theorem eqneqall 2962

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ≠ wne 2951

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 2952

This theorem is referenced by:  nonconne  2963  ssprsseq  4718  prnebg  4746  preqsnd  4749  preq12nebg  4753  prel12g  4754  opthprneg  4755  3elpr2eq  4800  snopeqop  5369  propssopi  5371  opthhausdorff  5380  opthhausdorff0  5381  iunopeqop  5384  tpres  6960  elovmpt3imp  7404  bropopvvv  7796  bropfvvvvlem  7797  infsupprpr  9014  epnsym  9118  eldju2ndl  9399  eldju2ndr  9400  fin1a2lem10  9882  modfzo0difsn  13373  suppssfz  13424  hashrabsn1  13798  hash2pwpr  13899  hashle2pr  13900  hashge2el2difr  13904  cshwidxmod  14225  cshwidx0  14228  mod2eq1n2dvds  15761  nno  15796  prm2orodd  16100  prm23lt5  16219  dvdsprmpweqnn  16289  symgextf1  18629  01eq0ring  20126  mamufacex  21104  mavmulsolcl  21264  chfacfscmulgsum  21573  chfacfpmmulgsum  21577  logbgcd1irr  25492  lgsqrmodndvds  26049  gausslemma2dlem0f  26057  gausslemma2dlem0i  26060  2lgs  26103  2lgsoddprm  26112  2sqreultlem  26143  2sqreunnltlem  26146  umgrnloop2  27051  uhgr2edg  27110  uvtx01vtx  27299  g0wlk0  27553  wlkreslem  27571  upgrwlkdvdelem  27637  uspgrn2crct  27706  wspn0  27822  2pthdlem1  27828  2pthon3v  27841  umgr2adedgspth  27846  umgrclwwlkge2  27888  lppthon  28048  1pthon2v  28050  frgrwopreglem4a  28207  frgrreg  28291  frgrregord13  28293  frgrogt3nreg  28294  nsnlplig  28376  nsnlpligALT  28377  gonarlem  32884  gonar  32885  goalrlem  32886  goalr  32887  bj-prmoore  34844  prproropf1olem4  44440  paireqne  44445  goldbachth  44481  lighneallem2  44540  lighneal  44545  requad1  44556  evenltle  44651  fppr2odd  44665  lidldomn1  44961  nzerooringczr  45112  ztprmneprm  45165  suppmptcfin  45197  linc1  45248  lindsrng01  45291  ldepspr  45296  zlmodzxznm  45320  rrx2xpref1o  45546  rrx2plord2  45550  line2ylem  45579  line2xlem  45581  line2y  45583  inlinecirc02plem  45614