Theorem eqneqall 2936

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  nonconne  2937  ssprsseq  4779  prnebg  4810  preqsnd  4813  preq12nebg  4817  prel12g  4818  opthprneg  4819  3elpr2eq  4860  snopeqop  5453  propssopi  5455  opthhausdorff  5464  opthhausdorff0  5465  iunopeqop  5468  tpres  7141  f1ounsn  7213  fvf1pr  7248  elovmpt3imp  7610  resf1extb  7874  bropopvvv  8030  bropfvvvvlem  8031  infsupprpr  9415  epnsym  9524  eldju2ndl  9839  eldju2ndr  9840  fin1a2lem10  10322  fvf1tp  13712  modfzo0difsn  13869  suppssfz  13920  hashrabsn1  14300  hash2pwpr  14402  hashle2pr  14403  hashge2el2difr  14407  cshwidxmod  14728  cshwidx0  14731  mod2eq1n2dvds  16277  nno  16312  prm2orodd  16621  prm23lt5  16745  dvdsprmpweqnn  16816  symgextf1  19319  01eq0ringOLD  20435  nzerooringczr  21406  mamufacex  22300  mavmulsolcl  22455  chfacfscmulgsum  22764  chfacfpmmulgsum  22768  logbgcd1irr  26721  lgsqrmodndvds  27281  gausslemma2dlem0f  27289  gausslemma2dlem0i  27292  2lgs  27335  2lgsoddprm  27344  2sqreultlem  27375  2sqreunnltlem  27378  sltlend  27700  umgrnloop2  29110  uhgr2edg  29172  uvtx01vtx  29361  g0wlk0  29615  wlkreslem  29632  upgrwlkdvdelem  29700  uspgrn2crct  29772  wspn0  29888  2pthdlem1  29894  2pthon3v  29907  umgr2adedgspth  29912  umgrclwwlkge2  29954  lppthon  30114  1pthon2v  30116  frgrwopreglem4a  30273  frgrreg  30357  frgrregord13  30359  frgrogt3nreg  30360  nsnlplig  30444  nsnlpligALT  30445  gonarlem  35386  gonar  35387  goalrlem  35388  goalr  35389  bj-prmoore  37108  prproropf1olem4  47510  paireqne  47515  goldbachth  47551  lighneallem2  47610  lighneal  47615  requad1  47626  evenltle  47721  fppr2odd  47735  elclnbgrelnbgr  47829  vopnbgrelself  47859  dfnbgr6  47861  isubgr3stgrlem4  47973  isubgr3stgrlem7  47976  gpgvtxedg0  48067  gpgvtxedg1  48068  gpgedgiov  48069  gpgedg2ov  48070  gpgedg2iv  48071  gpgprismgr4cycllem7  48105  pgnioedg1  48112  pgnioedg2  48113  pgnioedg3  48114  pgnioedg4  48115  pgnioedg5  48116  pgnbgreunbgrlem1  48117  pgnbgreunbgrlem2lem1  48118  pgnbgreunbgrlem2lem2  48119  pgnbgreunbgrlem2lem3  48120  pgnbgreunbgrlem2  48121  pgnbgreunbgrlem4  48123  pgnbgreunbgrlem5lem1  48124  pgnbgreunbgrlem5lem2  48125  pgnbgreunbgrlem5  48127  lidldomn1  48235  ztprmneprm  48351  suppmptcfin  48380  linc1  48430  lindsrng01  48473  ldepspr  48478  zlmodzxznm  48502  rrx2xpref1o  48723  rrx2plord2  48727  line2ylem  48756  line2xlem  48758  line2y  48760  inlinecirc02plem  48791