Theorem nesymi 2328

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

Syntax hints:   -. wn 3   = wceq 1314   =/= wne 2282

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-5 1406  ax-gen 1408  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-ne 2283

This theorem is referenced by:  frec0g  6248  djune  6915  omp1eomlem  6931  fodjum  6968  fodju0  6969  ismkvnex  6979  mkvprop  6982  xrltnr  9459  nltmnf  9467  xnn0xadd0  9543  pwle2  12885  nninfalllem1  12895  nninfall  12896  nninfsellemeq  12902