Theorem nesymi 2373

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

Syntax hints:   -. wn 3   = wceq 1335   =/= wne 2327

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-5 1427  ax-gen 1429  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-cleq 2150  df-ne 2328

This theorem is referenced by:  frec0g  6338  djune  7012  omp1eomlem  7028  fodjum  7072  fodju0  7073  ismkvnex  7081  mkvprop  7084  omniwomnimkv  7093  3nelsucpw1  7152  xrltnr  9668  nltmnf  9677  xnn0xadd0  9753  pwle2  13530  nninfalllem1  13542  nninfall  13543  nninfsellemeq  13548  trirec0xor  13578