Theorem eqneqall 2939

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2928

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 207  df-ne 2929

This theorem is referenced by:  nonconne  2940  ssprsseq  4772  prnebg  4803  preqsnd  4806  preq12nebg  4810  prel12g  4811  opthprneg  4812  3elpr2eq  4853  snopeqop  5441  propssopi  5443  opthhausdorff  5452  opthhausdorff0  5453  iunopeqop  5456  tpres  7130  f1ounsn  7201  fvf1pr  7236  elovmpt3imp  7598  resf1extb  7859  bropopvvv  8015  bropfvvvvlem  8016  infsupprpr  9385  epnsym  9494  eldju2ndl  9812  eldju2ndr  9813  fin1a2lem10  10295  fvf1tp  13688  modfzo0difsn  13845  suppssfz  13896  hashrabsn1  14276  hash2pwpr  14378  hashle2pr  14379  hashge2el2difr  14383  cshwidxmod  14705  cshwidx0  14708  mod2eq1n2dvds  16253  nno  16288  prm2orodd  16597  prm23lt5  16721  dvdsprmpweqnn  16792  symgextf1  19328  01eq0ringOLD  20441  nzerooringczr  21412  mamufacex  22306  mavmulsolcl  22461  chfacfscmulgsum  22770  chfacfpmmulgsum  22774  logbgcd1irr  26726  lgsqrmodndvds  27286  gausslemma2dlem0f  27294  gausslemma2dlem0i  27297  2lgs  27340  2lgsoddprm  27349  2sqreultlem  27380  2sqreunnltlem  27383  sltlend  27705  umgrnloop2  29119  uhgr2edg  29181  uvtx01vtx  29370  g0wlk0  29624  wlkreslem  29641  upgrwlkdvdelem  29709  uspgrn2crct  29781  wspn0  29897  2pthdlem1  29903  2pthon3v  29916  umgr2adedgspth  29921  umgrclwwlkge2  29963  lppthon  30123  1pthon2v  30125  frgrwopreglem4a  30282  frgrreg  30366  frgrregord13  30368  frgrogt3nreg  30369  nsnlplig  30453  nsnlpligALT  30454  gonarlem  35430  gonar  35431  goalrlem  35432  goalr  35433  bj-prmoore  37149  prproropf1olem4  47537  paireqne  47542  goldbachth  47578  lighneallem2  47637  lighneal  47642  requad1  47653  evenltle  47748  fppr2odd  47762  elclnbgrelnbgr  47856  vopnbgrelself  47886  dfnbgr6  47888  isubgr3stgrlem4  48000  isubgr3stgrlem7  48003  gpgvtxedg0  48094  gpgvtxedg1  48095  gpgedgiov  48096  gpgedg2ov  48097  gpgedg2iv  48098  gpgprismgr4cycllem7  48132  pgnioedg1  48139  pgnioedg2  48140  pgnioedg3  48141  pgnioedg4  48142  pgnioedg5  48143  pgnbgreunbgrlem1  48144  pgnbgreunbgrlem2lem1  48145  pgnbgreunbgrlem2lem2  48146  pgnbgreunbgrlem2lem3  48147  pgnbgreunbgrlem2  48148  pgnbgreunbgrlem4  48150  pgnbgreunbgrlem5lem1  48151  pgnbgreunbgrlem5lem2  48152  pgnbgreunbgrlem5  48154  lidldomn1  48262  ztprmneprm  48378  suppmptcfin  48407  linc1  48457  lindsrng01  48500  ldepspr  48505  zlmodzxznm  48529  rrx2xpref1o  48750  rrx2plord2  48754  line2ylem  48783  line2xlem  48785  line2y  48787  inlinecirc02plem  48818