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 2042 | . 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) | |
2 | 1 | necon3bii 2243 | 1 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 ≠ wne 2204 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 ax-5 1336 ax-gen 1338 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-cleq 2033 df-ne 2206 |
This theorem is referenced by: necomi 2290 necomd 2291 0pss 3265 difprsn1 3503 difprsn2 3504 diftpsn3 3505 fndmdifcom 5273 fvpr1 5365 fvpr2 5366 fvpr1g 5367 fvtp1g 5369 fvtp2g 5370 fvtp3g 5371 fvtp2 5373 fvtp3 5374 zltlen 8319 nn0lt2 8322 qltlen 8575 fzofzim 9044 flqeqceilz 9160 |
Copyright terms: Public domain | W3C validator |