![]() |
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 2142 | . 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) | |
2 | 1 | necon3bii 2347 | 1 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ≠ wne 2309 |
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 1424 ax-gen 1426 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-cleq 2133 df-ne 2310 |
This theorem is referenced by: necomi 2394 necomd 2395 difprsn1 3667 difprsn2 3668 diftpsn3 3669 fndmdifcom 5534 fvpr1 5632 fvpr2 5633 fvpr1g 5634 fvtp1g 5636 fvtp2g 5637 fvtp3g 5638 fvtp2 5640 fvtp3 5641 zltlen 9153 nn0lt2 9156 qltlen 9459 fzofzim 9996 flqeqceilz 10122 isprm2lem 11833 prm2orodd 11843 |
Copyright terms: Public domain | W3C validator |