Theorem eqneqall 2995

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1522   ≠ wne 2984

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 208  df-ne 2985

This theorem is referenced by:  nonconne  2996  ssprsseq  4665  prnebg  4693  preqsnd  4696  preq12nebg  4700  prel12g  4701  opthprneg  4702  3elpr2eq  4744  snopeqop  5287  propssopi  5289  opthhausdorff  5298  opthhausdorff0  5299  iunopeqop  5302  tpres  6830  elovmpt3imp  7260  bropopvvv  7641  bropfvvvvlem  7642  infsupprpr  8814  epnsym  8918  eldju2ndl  9199  eldju2ndr  9200  fin1a2lem10  9677  modfzo0difsn  13161  suppssfz  13212  hashrabsn1  13583  hash2pwpr  13680  hashle2pr  13681  hashge2el2difr  13685  cshwidxmod  14001  cshwidx0  14004  mod2eq1n2dvds  15529  nno  15566  prm2orodd  15864  prm23lt5  15980  dvdsprmpweqnn  16050  symgextf1  18280  01eq0ring  19734  mamufacex  20682  mavmulsolcl  20844  chfacfscmulgsum  21152  chfacfpmmulgsum  21156  logbgcd1irr  25053  lgsqrmodndvds  25611  gausslemma2dlem0f  25619  gausslemma2dlem0i  25622  2lgs  25665  2lgsoddprm  25674  2sqreultlem  25705  2sqreunnltlem  25708  umgrnloop2  26614  uhgr2edg  26673  uvtx01vtx  26862  g0wlk0  27116  wlkreslem  27134  wlkreslemOLD  27136  upgrwlkdvdelem  27204  uspgrn2crct  27273  wspn0  27390  2pthdlem1  27396  2pthon3v  27409  umgr2adedgspth  27414  umgrclwwlkge2  27456  lppthon  27617  1pthon2v  27619  frgrwopreglem4a  27781  frgrreg  27865  frgrregord13  27867  frgrogt3nreg  27868  nsnlplig  27949  nsnlpligALT  27950  gonarlem  32249  gonar  32250  goalrlem  32251  goalr  32252  prproropf1olem4  43150  paireqne  43155  goldbachth  43191  lighneallem2  43253  lighneal  43258  requad1  43269  evenltle  43364  fppr2odd  43378  lidldomn1  43670  nzerooringczr  43821  ztprmneprm  43873  suppmptcfin  43907  linc1  43960  lindsrng01  44003  ldepspr  44008  zlmodzxznm  44032  rrx2xpref1o  44186  rrx2plord2  44190  line2ylem  44219  line2xlem  44221  line2y  44223  inlinecirc02plem  44254