Theorem nesymi 2424

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

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

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 1471  ax-gen 1473  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-ne 2379

This theorem is referenced by:  frec0g  6506  djune  7206  omp1eomlem  7222  fodjum  7274  fodju0  7275  ismkvnex  7283  mkvprop  7286  omniwomnimkv  7295  pr2cv1  7329  3nelsucpw1  7380  xrltnr  9936  nltmnf  9945  xnn0xadd0  10024  fnpr2ob  13287  2lgslem3  15693  2lgslem4  15695  structiedg0val  15754  2omap  16132  pwle2  16137  nninfalllem1  16147  nninfall  16148  nninfsellemeq  16153  trirec0xor  16186