Theorem nesymi 2466

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

Syntax hints:  ¬ wn 3   = wceq 1402   ≠ wne 2420

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 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-ne 2421

This theorem is referenced by:  frec0g  6662  2omap  7312  djune  7412  omp1eomlem  7428  fodjum  7480  fodju0  7481  ismkvnex  7489  mkvprop  7492  omniwomnimkv  7501  pr2cv1  7535  3nelsucpw1  7587  xrltnr  10164  nltmnf  10173  xnn0xadd0  10252  ballotfilemi1  13228  fnpr2ob  13644  2lgslem3  16203  2lgslem4  16205  structiedg0val  16264  3dom  17001  pwle2  17011  exmidpeirce  17020  nninfalllem1  17025  nninfall  17026  nninfsellemeq  17031  trirec0xor  17068