Theorem nesymi 2448

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

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

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 1495  ax-gen 1497  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-ne 2403

This theorem is referenced by:  frec0g  6563  djune  7277  omp1eomlem  7293  fodjum  7345  fodju0  7346  ismkvnex  7354  mkvprop  7357  omniwomnimkv  7366  pr2cv1  7400  3nelsucpw1  7452  xrltnr  10014  nltmnf  10023  xnn0xadd0  10102  fnpr2ob  13425  2lgslem3  15833  2lgslem4  15835  structiedg0val  15894  3dom  16608  2omap  16615  pwle2  16620  nninfalllem1  16631  nninfall  16632  nninfsellemeq  16637  trirec0xor  16670