Theorem nesymi 2413

Description: Inference associated with nesym 2412. (Contributed by BJ, 7-Jul-2018.)

Hypothesis

Ref	Expression
nesymi.1	⊢ 𝐴 ≠ 𝐵

Assertion

Ref	Expression
nesymi	⊢ ¬ 𝐵 = 𝐴

Proof of Theorem nesymi

Step	Hyp	Ref	Expression
1		nesymi.1	. 2 ⊢ 𝐴 ≠ 𝐵
2		nesym 2412	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴)
3	1, 2	mpbi 145	1 ⊢ ¬ 𝐵 = 𝐴

Syntax hints:  ¬ wn 3   = wceq 1364   ≠ wne 2367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-5 1461  ax-gen 1463  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-ne 2368

This theorem is referenced by:  frec0g  6464  djune  7153  omp1eomlem  7169  fodjum  7221  fodju0  7222  ismkvnex  7230  mkvprop  7233  omniwomnimkv  7242  3nelsucpw1  7317  xrltnr  9871  nltmnf  9880  xnn0xadd0  9959  fnpr2ob  13042  2lgslem3  15426  2lgslem4  15428  2omap  15726  pwle2  15729  nninfalllem1  15739  nninfall  15740  nninfsellemeq  15745  trirec0xor  15776