Theorem nesymi 2458

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

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

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 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-ne 2413

This theorem is referenced by:  frec0g  6627  2omap  7268  djune  7368  omp1eomlem  7384  fodjum  7436  fodju0  7437  ismkvnex  7445  mkvprop  7448  omniwomnimkv  7457  pr2cv1  7491  3nelsucpw1  7543  xrltnr  10108  nltmnf  10117  xnn0xadd0  10196  fnpr2ob  13542  2lgslem3  15961  2lgslem4  15963  structiedg0val  16022  3dom  16749  pwle2  16759  exmidpeirce  16768  nninfalllem1  16773  nninfall  16774  nninfsellemeq  16779  trirec0xor  16816