Theorem eqneqall 2957

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2946

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 2947

This theorem is referenced by:  nonconne  2958  ssprsseq  4850  prnebg  4880  preqsnd  4883  preq12nebg  4887  prel12g  4888  opthprneg  4889  3elpr2eq  4930  snopeqop  5525  propssopi  5527  opthhausdorff  5536  opthhausdorff0  5537  iunopeqop  5540  tpres  7238  fvf1pr  7343  elovmpt3imp  7707  bropopvvv  8131  bropfvvvvlem  8132  infsupprpr  9573  epnsym  9678  eldju2ndl  9993  eldju2ndr  9994  fin1a2lem10  10478  fvf1tp  13840  modfzo0difsn  13994  suppssfz  14045  hashrabsn1  14423  hash2pwpr  14525  hashle2pr  14526  hashge2el2difr  14530  cshwidxmod  14851  cshwidx0  14854  mod2eq1n2dvds  16395  nno  16430  prm2orodd  16738  prm23lt5  16861  dvdsprmpweqnn  16932  symgextf1  19463  01eq0ringOLD  20557  nzerooringczr  21514  mamufacex  22421  mavmulsolcl  22578  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  logbgcd1irr  26855  lgsqrmodndvds  27415  gausslemma2dlem0f  27423  gausslemma2dlem0i  27426  2lgs  27469  2lgsoddprm  27478  2sqreultlem  27509  2sqreunnltlem  27512  sltlend  27834  umgrnloop2  29181  uhgr2edg  29243  uvtx01vtx  29432  g0wlk0  29688  wlkreslem  29705  upgrwlkdvdelem  29772  uspgrn2crct  29841  wspn0  29957  2pthdlem1  29963  2pthon3v  29976  umgr2adedgspth  29981  umgrclwwlkge2  30023  lppthon  30183  1pthon2v  30185  frgrwopreglem4a  30342  frgrreg  30426  frgrregord13  30428  frgrogt3nreg  30429  nsnlplig  30513  nsnlpligALT  30514  gonarlem  35362  gonar  35363  goalrlem  35364  goalr  35365  bj-prmoore  37081  prproropf1olem4  47380  paireqne  47385  goldbachth  47421  lighneallem2  47480  lighneal  47485  requad1  47496  evenltle  47591  fppr2odd  47605  vopnbgrelself  47727  dfnbgr6  47729  lidldomn1  47954  ztprmneprm  48072  suppmptcfin  48104  linc1  48154  lindsrng01  48197  ldepspr  48202  zlmodzxznm  48226  rrx2xpref1o  48452  rrx2plord2  48456  line2ylem  48485  line2xlem  48487  line2y  48489  inlinecirc02plem  48520