Theorem nesymi 2423

Description: Inference associated with nesym 2422. (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 2422	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴)
3	1, 2	mpbi 145	1 ⊢ ¬ 𝐵 = 𝐴

Syntax hints:  ¬ wn 3   = wceq 1373   ≠ wne 2377

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 1471  ax-gen 1473  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-ne 2378

This theorem is referenced by:  frec0g  6490  djune  7187  omp1eomlem  7203  fodjum  7255  fodju0  7256  ismkvnex  7264  mkvprop  7267  omniwomnimkv  7276  3nelsucpw1  7353  xrltnr  9908  nltmnf  9917  xnn0xadd0  9996  fnpr2ob  13216  2lgslem3  15622  2lgslem4  15624  structiedg0val  15683  2omap  16006  pwle2  16009  nninfalllem1  16019  nninfall  16020  nninfsellemeq  16025  trirec0xor  16058