Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nesymi | GIF version |
Description: Inference associated with nesym 2372. (Contributed by BJ, 7-Jul-2018.) |
Ref | Expression |
---|---|
nesymi.1 | ⊢ 𝐴 ≠ 𝐵 |
Ref | Expression |
---|---|
nesymi | ⊢ ¬ 𝐵 = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nesymi.1 | . 2 ⊢ 𝐴 ≠ 𝐵 | |
2 | nesym 2372 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴) | |
3 | 1, 2 | mpbi 144 | 1 ⊢ ¬ 𝐵 = 𝐴 |
Colors of variables: wff set class |
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 6344 djune 7022 omp1eomlem 7038 fodjum 7089 fodju0 7090 ismkvnex 7098 mkvprop 7101 omniwomnimkv 7110 3nelsucpw1 7169 xrltnr 9686 nltmnf 9695 xnn0xadd0 9771 pwle2 13581 nninfalllem1 13591 nninfall 13592 nninfsellemeq 13597 trirec0xor 13627 |
Copyright terms: Public domain | W3C validator |