Theorem nesymi 2466

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

This proof depends on syntax axioms:   -. wn 3   = wceq 1402   =/= wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-ne 2421

This theorem is used by:  frec0g  6673  2omap  7324  djune  7424  omp1eomlem  7440  fodjum  7492  fodju0  7493  ismkvnex  7501  mkvprop  7504  omniwomnimkv  7513  pr2cv1  7547  3nelsucpw1  7599  xrltnr  10197  nltmnf  10206  xnn0xadd0  10285  ballotfilemi1  13302  fnpr2ob  13719  2lgslem3  16442  2lgslem4  16444  structiedg0val  16503  3dom  17240  pwle2  17250  exmidpeirce  17260  wexmiddifxylem  17267  nninfalllem1  17274  nninfall  17275  nninfsellemeq  17280  trirec0xor  17318