Theorem nesymi 2448

Description: Inference associated with nesym 2447. (Contributed by BJ, 7-Jul-2018.)

Hypothesis

Ref	Expression
nesymi.1	|- A =/= B

Assertion

Ref	Expression
nesymi	|- -. B = A

Proof of Theorem nesymi

Step	Hyp	Ref	Expression
1		nesymi.1	. 2 |- A =/= B
2		nesym 2447	. 2 |- ( A =/= B <-> -. B = A )
3	1, 2	mpbi 145	1 |- -. B = A

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  6562  djune  7276  omp1eomlem  7292  fodjum  7344  fodju0  7345  ismkvnex  7353  mkvprop  7356  omniwomnimkv  7365  pr2cv1  7399  3nelsucpw1  7451  xrltnr  10013  nltmnf  10022  xnn0xadd0  10101  fnpr2ob  13422  2lgslem3  15829  2lgslem4  15831  structiedg0val  15890  3dom  16587  2omap  16594  pwle2  16599  nninfalllem1  16610  nninfall  16611  nninfsellemeq  16616  trirec0xor  16649