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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1559   ≠ wne 2956

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 209  df-ne 2957

This theorem is referenced by:  nonconne  2968  ssprsseq  4780  prnebg  4811  preqsnd  4814  preq12nebg  4818  prel12g  4819  opthprneg  4820  3elpr2eq  4861  snopeqop  5472  propssopi  5474  opthhausdorff  5483  opthhausdorff0  5484  iunopeqop  5487  iunopeqopOLD  5488  tpres  7180  f1ounsn  7251  fvf1pr  7286  elovmpt3imp  7648  resf1extb  7910  bropopvvv  8063  bropfvvvvlem  8064  infsupprpr  9446  epnsym  9558  eldju2ndl  9876  eldju2ndr  9877  fin1a2lem10  10360  fvf1tp  13793  modfzo0difsn  13950  suppssfz  14001  hashrabsn1  14381  hash2pwpr  14483  hashle2pr  14484  hashge2el2difr  14488  cshwidxmod  14810  cshwidx0  14813  mod2eq1n2dvds  16372  nno  16407  prm2orodd  16716  prm23lt5  16841  dvdsprmpweqnn  16912  symgextf1  19452  01eq0ringOLD  20568  nzerooringczr  21520  mamufacex  22444  mavmulsolcl  22599  chfacfscmulgsum  22908  chfacfpmmulgsum  22912  logbgcd1irr  26847  lgsqrmodndvds  27405  gausslemma2dlem0f  27413  gausslemma2dlem0i  27416  2lgs  27459  2lgsoddprm  27468  2sqreultlem  27499  2sqreunnltlem  27502  ltlesnd  27827  umgrnloop2  29304  uhgr2edg  29366  uvtx01vtx  29555  g0wlk0  29808  wlkreslem  29825  upgrwlkdvdelem  29893  uspgrn2crct  29965  wspn0  30081  2pthdlem1  30087  2pthon3v  30100  umgr2adedgspth  30105  umgrclwwlkge2  30150  lppthon  30310  1pthon2v  30312  frgrwopreglem4a  30469  frgrreg  30553  frgrregord13  30555  frgrogt3nreg  30556  nsnlplig  30641  nsnlpligALT  30642  gonarlem  35705  gonar  35706  goalrlem  35707  goalr  35708  bj-prmoore  37566  prproropf1olem4  48073  paireqne  48078  goldbachth  48117  lighneallem2  48176  lighneal  48181  requad1  48205  evenltle  48300  fppr2odd  48314  elclnbgrelnbgr  48408  vopnbgrelself  48438  dfnbgr6  48440  isubgr3stgrlem4  48552  isubgr3stgrlem7  48555  gpgvtxedg0  48646  gpgvtxedg1  48647  gpgedgiov  48648  gpgedg2ov  48649  gpgedg2iv  48650  gpgprismgr4cycllem7  48684  pgnioedg1  48691  pgnioedg2  48692  pgnioedg3  48693  pgnioedg4  48694  pgnioedg5  48695  pgnbgreunbgrlem1  48696  pgnbgreunbgrlem2lem1  48697  pgnbgreunbgrlem2lem2  48698  pgnbgreunbgrlem2lem3  48699  pgnbgreunbgrlem2  48700  pgnbgreunbgrlem4  48702  pgnbgreunbgrlem5lem1  48703  pgnbgreunbgrlem5lem2  48704  pgnbgreunbgrlem5  48706  lidldomn1  48814  ztprmneprm  48930  suppmptcfin  48959  linc1  49008  lindsrng01  49051  ldepspr  49056  zlmodzxznm  49080  rrx2xpref1o  49301  rrx2plord2  49305  line2ylem  49334  line2xlem  49336  line2y  49338  inlinecirc02plem  49369