Theorem nesymi 2422

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

Syntax hints:   -. wn 3   = wceq 1373   =/= wne 2376

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 615  ax-in2 616  ax-5 1470  ax-gen 1472  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-ne 2377

This theorem is referenced by:  frec0g  6483  djune  7180  omp1eomlem  7196  fodjum  7248  fodju0  7249  ismkvnex  7257  mkvprop  7260  omniwomnimkv  7269  3nelsucpw1  7346  xrltnr  9901  nltmnf  9910  xnn0xadd0  9989  fnpr2ob  13172  2lgslem3  15578  2lgslem4  15580  structiedg0val  15637  2omap  15932  pwle2  15935  nninfalllem1  15945  nninfall  15946  nninfsellemeq  15951  trirec0xor  15984