Theorem eqneqall 2410

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1395   ≠ wne 2400

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

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

This theorem is referenced by:  ssprsseq  3830  eldju2ndl  7250  eldju2ndr  7251  modfzo0difsn  10629  nno  12432  prm2orodd  12663  prm23lt5  12801  dvdsprmpweqnn  12874  logbgcd1irr  15656  gausslemma2dlem0f  15748  gausslemma2dlem0i  15751  2lgs  15798  2lgsoddprm  15807  umgrnloop2  15964  uhgr2edg  16019  umgrclwwlkge2  16139