Theorem nesymi 2447

Description: Inference associated with nesym 2446. (Contributed by BJ, 7-Jul-2018.)

Hypothesis

Ref	Expression
nesymi.1	⊢ 𝐴 ≠ 𝐵

Assertion

Ref	Expression
nesymi	⊢ ¬ 𝐵 = 𝐴

Proof of Theorem nesymi

Step	Hyp	Ref	Expression
1		nesymi.1	. 2 ⊢ 𝐴 ≠ 𝐵
2		nesym 2446	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴)
3	1, 2	mpbi 145	1 ⊢ ¬ 𝐵 = 𝐴

Syntax hints:  ¬ wn 3   = wceq 1397   ≠ wne 2401

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 619  ax-in2 620  ax-5 1495  ax-gen 1497  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-cleq 2223  df-ne 2402

This theorem is referenced by:  frec0g  6568  djune  7282  omp1eomlem  7298  fodjum  7350  fodju0  7351  ismkvnex  7359  mkvprop  7362  omniwomnimkv  7371  pr2cv1  7405  3nelsucpw1  7457  xrltnr  10019  nltmnf  10028  xnn0xadd0  10107  fnpr2ob  13446  2lgslem3  15859  2lgslem4  15861  structiedg0val  15920  3dom  16647  2omap  16654  pwle2  16659  exmidpeirce  16668  nninfalllem1  16673  nninfall  16674  nninfsellemeq  16679  trirec0xor  16716