Theorem eqneqall 2413

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

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

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 2404

This theorem is referenced by:  ssprsseq  3840  eldju2ndl  7314  eldju2ndr  7315  modfzo0difsn  10703  nno  12530  prm2orodd  12761  prm23lt5  12899  dvdsprmpweqnn  12972  logbgcd1irr  15761  gausslemma2dlem0f  15856  gausslemma2dlem0i  15859  2lgs  15906  2lgsoddprm  15915  umgrnloop2  16075  uhgr2edg  16130  umgrclwwlkge2  16326