Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nesymi | GIF version |
Description: Inference associated with nesym 2385. (Contributed by BJ, 7-Jul-2018.) |
Ref | Expression |
---|---|
nesymi.1 | ⊢ 𝐴 ≠ 𝐵 |
Ref | Expression |
---|---|
nesymi | ⊢ ¬ 𝐵 = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nesymi.1 | . 2 ⊢ 𝐴 ≠ 𝐵 | |
2 | nesym 2385 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴) | |
3 | 1, 2 | mpbi 144 | 1 ⊢ ¬ 𝐵 = 𝐴 |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 = wceq 1348 ≠ wne 2340 |
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 609 ax-in2 610 ax-5 1440 ax-gen 1442 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-cleq 2163 df-ne 2341 |
This theorem is referenced by: frec0g 6376 djune 7055 omp1eomlem 7071 fodjum 7122 fodju0 7123 ismkvnex 7131 mkvprop 7134 omniwomnimkv 7143 3nelsucpw1 7211 xrltnr 9736 nltmnf 9745 xnn0xadd0 9824 pwle2 14031 nninfalllem1 14041 nninfall 14042 nninfsellemeq 14047 trirec0xor 14077 |
Copyright terms: Public domain | W3C validator |