Theorem eqneqall 2412

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1397   ≠ wne 2402

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 2403

This theorem is referenced by:  ssprsseq  3835  eldju2ndl  7271  eldju2ndr  7272  modfzo0difsn  10658  nno  12472  prm2orodd  12703  prm23lt5  12841  dvdsprmpweqnn  12914  logbgcd1irr  15697  gausslemma2dlem0f  15789  gausslemma2dlem0i  15792  2lgs  15839  2lgsoddprm  15848  umgrnloop2  16008  uhgr2edg  16063  umgrclwwlkge2  16259