Theorem eqneqall 2945

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ≠ wne 2934

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 2935

This theorem is referenced by:  nonconne  2946  ssprsseq  4757  prnebg  4788  preqsnd  4791  preq12nebg  4795  prel12g  4796  opthprneg  4797  3elpr2eq  4838  snopeqop  5448  propssopi  5450  opthhausdorff  5459  opthhausdorff0  5460  iunopeqop  5463  iunopeqopOLD  5464  tpres  7146  f1ounsn  7217  fvf1pr  7252  elovmpt3imp  7614  resf1extb  7875  bropopvvv  8030  bropfvvvvlem  8031  infsupprpr  9410  epnsym  9522  eldju2ndl  9840  eldju2ndr  9841  fin1a2lem10  10323  fvf1tp  13740  modfzo0difsn  13897  suppssfz  13948  hashrabsn1  14328  hash2pwpr  14430  hashle2pr  14431  hashge2el2difr  14435  cshwidxmod  14757  cshwidx0  14760  mod2eq1n2dvds  16308  nno  16343  prm2orodd  16652  prm23lt5  16777  dvdsprmpweqnn  16848  symgextf1  19388  01eq0ringOLD  20504  nzerooringczr  21456  mamufacex  22380  mavmulsolcl  22535  chfacfscmulgsum  22844  chfacfpmmulgsum  22848  logbgcd1irr  26777  lgsqrmodndvds  27335  gausslemma2dlem0f  27343  gausslemma2dlem0i  27346  2lgs  27389  2lgsoddprm  27398  2sqreultlem  27429  2sqreunnltlem  27432  ltlesnd  27758  umgrnloop2  29234  uhgr2edg  29296  uvtx01vtx  29485  g0wlk0  29738  wlkreslem  29755  upgrwlkdvdelem  29823  uspgrn2crct  29895  wspn0  30011  2pthdlem1  30017  2pthon3v  30030  umgr2adedgspth  30035  umgrclwwlkge2  30080  lppthon  30240  1pthon2v  30242  frgrwopreglem4a  30399  frgrreg  30483  frgrregord13  30485  frgrogt3nreg  30486  nsnlplig  30571  nsnlpligALT  30572  gonarlem  35631  gonar  35632  goalrlem  35633  goalr  35634  bj-prmoore  37482  prproropf1olem4  47989  paireqne  47994  goldbachth  48033  lighneallem2  48092  lighneal  48097  requad1  48121  evenltle  48216  fppr2odd  48230  elclnbgrelnbgr  48324  vopnbgrelself  48354  dfnbgr6  48356  isubgr3stgrlem4  48468  isubgr3stgrlem7  48471  gpgvtxedg0  48562  gpgvtxedg1  48563  gpgedgiov  48564  gpgedg2ov  48565  gpgedg2iv  48566  gpgprismgr4cycllem7  48600  pgnioedg1  48607  pgnioedg2  48608  pgnioedg3  48609  pgnioedg4  48610  pgnioedg5  48611  pgnbgreunbgrlem1  48612  pgnbgreunbgrlem2lem1  48613  pgnbgreunbgrlem2lem2  48614  pgnbgreunbgrlem2lem3  48615  pgnbgreunbgrlem2  48616  pgnbgreunbgrlem4  48618  pgnbgreunbgrlem5lem1  48619  pgnbgreunbgrlem5lem2  48620  pgnbgreunbgrlem5  48622  lidldomn1  48730  ztprmneprm  48846  suppmptcfin  48875  linc1  48924  lindsrng01  48967  ldepspr  48972  zlmodzxznm  48996  rrx2xpref1o  49217  rrx2plord2  49221  line2ylem  49250  line2xlem  49252  line2y  49254  inlinecirc02plem  49285