![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nesymi | GIF version |
Description: Inference associated with nesym 2392. (Contributed by BJ, 7-Jul-2018.) |
Ref | Expression |
---|---|
nesymi.1 | ⊢ 𝐴 ≠ 𝐵 |
Ref | Expression |
---|---|
nesymi | ⊢ ¬ 𝐵 = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nesymi.1 | . 2 ⊢ 𝐴 ≠ 𝐵 | |
2 | nesym 2392 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴) | |
3 | 1, 2 | mpbi 145 | 1 ⊢ ¬ 𝐵 = 𝐴 |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 = wceq 1353 ≠ wne 2347 |
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 614 ax-in2 615 ax-5 1447 ax-gen 1449 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 df-ne 2348 |
This theorem is referenced by: frec0g 6397 djune 7076 omp1eomlem 7092 fodjum 7143 fodju0 7144 ismkvnex 7152 mkvprop 7155 omniwomnimkv 7164 3nelsucpw1 7232 xrltnr 9777 nltmnf 9786 xnn0xadd0 9865 pwle2 14630 nninfalllem1 14639 nninfall 14640 nninfsellemeq 14645 trirec0xor 14675 |
Copyright terms: Public domain | W3C validator |