![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > necom | GIF version |
Description: Commutation of inequality. (Contributed by NM, 14-May-1999.) |
Ref | Expression |
---|---|
necom | ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqcom 2195 | . 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) | |
2 | 1 | necon3bii 2402 | 1 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 ≠ wne 2364 |
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 615 ax-in2 616 ax-5 1458 ax-gen 1460 ax-ext 2175 |
This theorem depends on definitions: df-bi 117 df-cleq 2186 df-ne 2365 |
This theorem is referenced by: necomi 2449 necomd 2450 difprsn1 3758 difprsn2 3759 diftpsn3 3760 fndmdifcom 5665 fvpr1 5763 fvpr2 5764 fvpr1g 5765 fvtp1g 5767 fvtp2g 5768 fvtp3g 5769 fvtp2 5771 fvtp3 5772 netap 7316 2omotaplemap 7319 zltlen 9398 nn0lt2 9401 qltlen 9708 fzofzim 10258 flqeqceilz 10392 isprm2lem 12257 prm2orodd 12267 tridceq 15616 |
Copyright terms: Public domain | W3C validator |