Theorem eqneqall 2967

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2957

This theorem is used by:  nonconne  2968  ssprsseq  4786  prnebg  4816  preqsnd  4819  preq12nebg  4823  prel12g  4824  opthprneg  4825  3elpr2eq  4866  snopeqop  5478  propssopi  5480  opthhausdorff  5490  opthhausdorff0  5491  iunopeqop  5494  iunopeqopOLD  5495  tpres  7205  f1ounsn  7278  fvf1pr  7313  elovmpt3imp  7676  resf1extb  7944  bropopvvv  8099  bropfvvvvlem  8100  infsupprpr  9491  epnsym  9603  eldju2ndl  9998  eldju2ndr  9999  fin1a2lem10  10480  fvf1tp  13922  modfzo0difsn  14079  suppssfz  14130  hashrabsn1  14511  hash2pwpr  14614  hashle2pr  14615  hashge2el2difr  14619  cshwidxmod  14947  cshwidx0  14950  mod2eq1n2dvds  16510  nno  16545  prm2orodd  16859  prm23lt5  16985  dvdsprmpweqnn  17056  symgextf1  19628  01eq0ringOLD  20775  nzerooringczr  21779  mamufacex  22704  mavmulsolcl  22859  chfacfscmulgsum  23171  chfacfpmmulgsum  23175  logbgcd1irr  27115  lgsqrmodndvds  27673  gausslemma2dlem0f  27681  gausslemma2dlem0i  27684  2lgs  27727  2lgsoddprm  27736  2sqreultlem  27767  2sqreunnltlem  27770  ltlesnd  28125  umgrnloop2  29717  uhgr2edg  29782  uvtx01vtx  29971  g0wlk0  30224  wlkreslem  30241  upgrwlkdvdelem  30315  uspgrn2crct  30390  wspn0  30506  2pthdlem1  30512  2pthon3v  30525  umgr2adedgspth  30530  umgrclwwlkge2  30575  lppthon  30735  1pthon2v  30747  frgrwopreglem4a  30904  frgrreg  30988  frgrregord13  30990  frgrogt3nreg  30991  nsnlplig  31076  nsnlpligALT  31077  gonarlem  36138  gonar  36139  goalrlem  36140  goalr  36141  bj-prmoore  38016  prproropf1olem4  48557  paireqne  48562  goldbachth  48601  lighneallem2  48660  lighneal  48665  requad1  48689  evenltle  48784  fppr2odd  48798  elclnbgrelnbgr  48892  vopnbgrelself  48922  dfnbgr6  48924  isubgr3stgrlem4  49036  isubgr3stgrlem7  49039  gpgvtxedg0  49130  gpgvtxedg1  49131  gpgedgiov  49132  gpgedg2ov  49133  gpgedg2iv  49134  gpgprismgr4cycllem7  49168  pgnioedg1  49175  pgnioedg2  49176  pgnioedg3  49177  pgnioedg4  49178  pgnioedg5  49179  pgnbgreunbgrlem1  49180  pgnbgreunbgrlem2lem1  49181  pgnbgreunbgrlem2lem2  49182  pgnbgreunbgrlem2lem3  49183  pgnbgreunbgrlem2  49184  pgnbgreunbgrlem4  49186  pgnbgreunbgrlem5lem1  49187  pgnbgreunbgrlem5lem2  49188  pgnbgreunbgrlem5  49190  lidldomn1  49297  ztprmneprm  49428  suppmptcfin  49457  linc1  49506  lindsrng01  49549  ldepspr  49554  zlmodzxznm  49578  rrx2xpref1o  49799  rrx2plord2  49803  line2ylem  49832  line2xlem  49834  line2y  49836  inlinecirc02plem  49867