Theorem nesymi 2458

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

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  6628  2omap  7269  djune  7369  omp1eomlem  7385  fodjum  7437  fodju0  7438  ismkvnex  7446  mkvprop  7449  omniwomnimkv  7458  pr2cv1  7492  3nelsucpw1  7544  xrltnr  10112  nltmnf  10121  xnn0xadd0  10200  fnpr2ob  13553  2lgslem3  15974  2lgslem4  15976  structiedg0val  16035  3dom  16762  pwle2  16772  exmidpeirce  16781  nninfalllem1  16786  nninfall  16787  nninfsellemeq  16792  trirec0xor  16829