Theorem eqneqall 2955

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2944

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 206  df-ne 2945

This theorem is referenced by:  nonconne  2956  ssprsseq  4759  prnebg  4787  preqsnd  4790  preq12nebg  4794  prel12g  4795  opthprneg  4796  3elpr2eq  4839  snopeqop  5421  propssopi  5423  opthhausdorff  5432  opthhausdorff0  5433  iunopeqop  5436  tpres  7085  elovmpt3imp  7535  bropopvvv  7939  bropfvvvvlem  7940  infsupprpr  9272  epnsym  9376  eldju2ndl  9691  eldju2ndr  9692  fin1a2lem10  10174  modfzo0difsn  13672  suppssfz  13723  hashrabsn1  14098  hash2pwpr  14199  hashle2pr  14200  hashge2el2difr  14204  cshwidxmod  14525  cshwidx0  14528  mod2eq1n2dvds  16065  nno  16100  prm2orodd  16405  prm23lt5  16524  dvdsprmpweqnn  16595  symgextf1  19038  01eq0ring  20552  mamufacex  21547  mavmulsolcl  21709  chfacfscmulgsum  22018  chfacfpmmulgsum  22022  logbgcd1irr  25953  lgsqrmodndvds  26510  gausslemma2dlem0f  26518  gausslemma2dlem0i  26521  2lgs  26564  2lgsoddprm  26573  2sqreultlem  26604  2sqreunnltlem  26607  umgrnloop2  27525  uhgr2edg  27584  uvtx01vtx  27773  g0wlk0  28028  wlkreslem  28046  upgrwlkdvdelem  28113  uspgrn2crct  28182  wspn0  28298  2pthdlem1  28304  2pthon3v  28317  umgr2adedgspth  28322  umgrclwwlkge2  28364  lppthon  28524  1pthon2v  28526  frgrwopreglem4a  28683  frgrreg  28767  frgrregord13  28769  frgrogt3nreg  28770  nsnlplig  28852  nsnlpligALT  28853  gonarlem  33365  gonar  33366  goalrlem  33367  goalr  33368  bj-prmoore  35295  prproropf1olem4  44969  paireqne  44974  goldbachth  45010  lighneallem2  45069  lighneal  45074  requad1  45085  evenltle  45180  fppr2odd  45194  lidldomn1  45490  nzerooringczr  45641  ztprmneprm  45694  suppmptcfin  45726  linc1  45777  lindsrng01  45820  ldepspr  45825  zlmodzxznm  45849  rrx2xpref1o  46075  rrx2plord2  46079  line2ylem  46108  line2xlem  46110  line2y  46112  inlinecirc02plem  46143