Theorem nesymi 2460

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

Syntax hints:  ¬ wn 3   = wceq 1398   ≠ wne 2414

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 619  ax-in2 620  ax-5 1496  ax-gen 1498  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-ne 2415

This theorem is referenced by:  frec0g  6630  2omap  7271  djune  7371  omp1eomlem  7387  fodjum  7439  fodju0  7440  ismkvnex  7448  mkvprop  7451  omniwomnimkv  7460  pr2cv1  7494  3nelsucpw1  7546  xrltnr  10118  nltmnf  10127  xnn0xadd0  10206  fnpr2ob  13574  2lgslem3  16023  2lgslem4  16025  structiedg0val  16084  3dom  16811  pwle2  16821  exmidpeirce  16830  nninfalllem1  16835  nninfall  16836  nninfsellemeq  16841  trirec0xor  16878