Theorem eqneqall 2422

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1398   ≠ wne 2412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-in2 620

This theorem depends on definitions:  df-bi 117  df-ne 2413

This theorem is referenced by:  ssprsseq  3856  eldju2ndl  7363  eldju2ndr  7364  modfzo0difsn  10757  nno  12592  prm2orodd  12823  prm23lt5  12961  dvdsprmpweqnn  13034  logbgcd1irr  15832  gausslemma2dlem0f  15927  gausslemma2dlem0i  15930  2lgs  15977  2lgsoddprm  15986  umgrnloop2  16146  uhgr2edg  16201  umgrclwwlkge2  16397