Theorem eqneqall 2971

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 2961	. 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 2960

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 2961

This theorem is used by:  nonconne  2972  ssprsseq  4793  prnebg  4823  preqsnd  4826  preq12nebg  4830  prel12g  4831  opthprneg  4832  3elpr2eq  4873  snopeqop  5491  propssopi  5493  opthhausdorff  5502  opthhausdorff0  5503  iunopeqop  5506  iunopeqopOLD  5507  tpres  7203  f1ounsn  7276  fvf1pr  7311  elovmpt3imp  7673  resf1extb  7933  bropopvvv  8087  bropfvvvvlem  8088  infsupprpr  9469  epnsym  9581  eldju2ndl  9922  eldju2ndr  9923  fin1a2lem10  10404  fvf1tp  13836  modfzo0difsn  13993  suppssfz  14044  hashrabsn1  14424  hash2pwpr  14527  hashle2pr  14528  hashge2el2difr  14532  cshwidxmod  14860  cshwidx0  14863  mod2eq1n2dvds  16423  nno  16458  prm2orodd  16767  prm23lt5  16892  dvdsprmpweqnn  16963  symgextf1  19515  01eq0ringOLD  20659  nzerooringczr  21660  mamufacex  22583  mavmulsolcl  22738  chfacfscmulgsum  23047  chfacfpmmulgsum  23051  logbgcd1irr  26990  lgsqrmodndvds  27548  gausslemma2dlem0f  27556  gausslemma2dlem0i  27559  2lgs  27602  2lgsoddprm  27611  2sqreultlem  27642  2sqreunnltlem  27645  ltlesnd  27970  umgrnloop2  29527  uhgr2edg  29592  uvtx01vtx  29781  g0wlk0  30034  wlkreslem  30051  upgrwlkdvdelem  30125  uspgrn2crct  30200  wspn0  30316  2pthdlem1  30322  2pthon3v  30335  umgr2adedgspth  30340  umgrclwwlkge2  30385  lppthon  30545  1pthon2v  30551  frgrwopreglem4a  30708  frgrreg  30792  frgrregord13  30794  frgrogt3nreg  30795  nsnlplig  30880  nsnlpligALT  30881  gonarlem  35899  gonar  35900  goalrlem  35901  goalr  35902  bj-prmoore  37790  prproropf1olem4  48288  paireqne  48293  goldbachth  48332  lighneallem2  48391  lighneal  48396  requad1  48420  evenltle  48515  fppr2odd  48529  elclnbgrelnbgr  48623  vopnbgrelself  48653  dfnbgr6  48655  isubgr3stgrlem4  48767  isubgr3stgrlem7  48770  gpgvtxedg0  48861  gpgvtxedg1  48862  gpgedgiov  48863  gpgedg2ov  48864  gpgedg2iv  48865  gpgprismgr4cycllem7  48899  pgnioedg1  48906  pgnioedg2  48907  pgnioedg3  48908  pgnioedg4  48909  pgnioedg5  48910  pgnbgreunbgrlem1  48911  pgnbgreunbgrlem2lem1  48912  pgnbgreunbgrlem2lem2  48913  pgnbgreunbgrlem2lem3  48914  pgnbgreunbgrlem2  48915  pgnbgreunbgrlem4  48917  pgnbgreunbgrlem5lem1  48918  pgnbgreunbgrlem5lem2  48919  pgnbgreunbgrlem5  48921  lidldomn1  49029  ztprmneprm  49160  suppmptcfin  49189  linc1  49238  lindsrng01  49281  ldepspr  49286  zlmodzxznm  49310  rrx2xpref1o  49531  rrx2plord2  49535  line2ylem  49564  line2xlem  49566  line2y  49568  inlinecirc02plem  49599