Theorem eqneqall 2966

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

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

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 2956

This theorem is used by:  nonconne  2967  ssprsseq  4780  prnebg  4810  preqsnd  4813  preq12nebg  4817  prel12g  4818  opthprneg  4819  3elpr2eq  4833  snopeqop  5477  propssopi  5479  opthhausdorff  5489  opthhausdorff0  5490  iunopeqop  5493  iunopeqopOLD  5494  tpres  7208  f1ounsn  7281  fvf1pr  7316  elovmpt3imp  7679  resf1extb  7947  bropopvvv  8102  bropfvvvvlem  8103  infsupprpr  9502  epnsym  9614  eldju2ndl  10009  eldju2ndr  10010  fin1a2lem10  10491  fvf1tp  13933  modfzo0difsn  14090  suppssfz  14141  hashrabsn1  14522  hash2pwpr  14625  hashle2pr  14626  hashge2el2difr  14630  cshwidxmod  14959  cshwidx0  14962  mod2eq1n2dvds  16523  nno  16558  prm2orodd  16872  prm23lt5  16998  dvdsprmpweqnn  17069  symgextf1  19641  01eq0ringOLD  20788  nzerooringczr  21792  mamufacex  22717  mavmulsolcl  22872  chfacfscmulgsum  23184  chfacfpmmulgsum  23188  logbgcd1irr  27128  lgsqrmodndvds  27686  gausslemma2dlem0f  27694  gausslemma2dlem0i  27697  2lgs  27740  2lgsoddprm  27749  2sqreultlem  27780  2sqreunnltlem  27783  ltlesnd  28138  umgrnloop2  29730  uhgr2edg  29795  uvtx01vtx  29984  g0wlk0  30237  wlkreslem  30254  upgrwlkdvdelem  30328  uspgrn2crct  30403  wspn0  30519  2pthdlem1  30525  2pthon3v  30538  umgr2adedgspth  30543  umgrclwwlkge2  30588  lppthon  30748  1pthon2v  30760  frgrwopreglem4a  30917  frgrreg  31001  frgrregord13  31003  frgrogt3nreg  31004  nsnlplig  31089  nsnlpligALT  31090  gonarlem  36246  gonar  36247  goalrlem  36248  goalr  36249  bj-prmoore  38129  prproropf1olem4  48682  paireqne  48687  goldbachth  48726  lighneallem2  48785  lighneal  48790  requad1  48814  evenltle  48909  fppr2odd  48923  elclnbgrelnbgr  49017  vopnbgrelself  49047  dfnbgr6  49049  isubgr3stgrlem4  49161  isubgr3stgrlem7  49164  gpgvtxedg0  49255  gpgvtxedg1  49256  gpgedgiov  49257  gpgedg2ov  49258  gpgedg2iv  49259  gpgprismgr4cycllem7  49293  pgnioedg1  49300  pgnioedg2  49301  pgnioedg3  49302  pgnioedg4  49303  pgnioedg5  49304  pgnbgreunbgrlem1  49305  pgnbgreunbgrlem2lem1  49306  pgnbgreunbgrlem2lem2  49307  pgnbgreunbgrlem2lem3  49308  pgnbgreunbgrlem2  49309  pgnbgreunbgrlem4  49311  pgnbgreunbgrlem5lem1  49312  pgnbgreunbgrlem5lem2  49313  pgnbgreunbgrlem5  49315  lidldomn1  49422  ztprmneprm  49553  suppmptcfin  49582  linc1  49631  lindsrng01  49674  ldepspr  49679  zlmodzxznm  49703  rrx2plord2  49929  line2ylem  49957  line2xlem  49959  line2y  49961  inlinecirc02plem  49992