Theorem eqneqall 2430

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1402   ≠ wne 2420

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

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

This theorem is referenced by:  ssprsseq  3872  eldju2ndl  7402  eldju2ndr  7403  modfzo0difsn  10810  nno  12651  prm2orodd  12882  prm23lt5  13020  dvdsprmpweqnn  13093  logbgcd1irr  15992  gausslemma2dlem0f  16087  gausslemma2dlem0i  16090  2lgs  16137  2lgsoddprm  16146  umgrnloop2  16306  uhgr2edg  16361  umgrclwwlkge2  16557