Theorem nesymi 2449

Description: Inference associated with nesym 2448. (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 2448	. 2 |- ( A =/= B <-> -. B = A )
3	1, 2	mpbi 145	1 |- -. B = A

Syntax hints:   -. wn 3   = wceq 1398   =/= wne 2403

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 2213

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

This theorem is referenced by:  frec0g  6606  djune  7320  omp1eomlem  7336  fodjum  7388  fodju0  7389  ismkvnex  7397  mkvprop  7400  omniwomnimkv  7409  pr2cv1  7443  3nelsucpw1  7495  xrltnr  10058  nltmnf  10067  xnn0xadd0  10146  fnpr2ob  13486  2lgslem3  15903  2lgslem4  15905  structiedg0val  15964  3dom  16691  2omap  16698  pwle2  16703  exmidpeirce  16712  nninfalllem1  16717  nninfall  16718  nninfsellemeq  16723  trirec0xor  16760