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  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  13441  2lgslem3  15849  2lgslem4  15851  structiedg0val  15910  3dom  16638  2omap  16645  pwle2  16650  nninfalllem1  16661  nninfall  16662  nninfsellemeq  16667  trirec0xor  16700