![]() |
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 | ⊢ (A ≠ B ↔ B ≠ A) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqcom 2039 | . 2 ⊢ (A = B ↔ B = A) | |
2 | 1 | necon3bii 2237 | 1 ⊢ (A ≠ B ↔ B ≠ A) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 ≠ wne 2201 |
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 1333 ax-gen 1335 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-cleq 2030 df-ne 2203 |
This theorem is referenced by: necomi 2284 necomd 2285 0pss 3259 difprsn1 3494 difprsn2 3495 diftpsn3 3496 fndmdifcom 5216 fvpr1 5308 fvpr2 5309 fvpr1g 5310 fvtp1g 5312 fvtp2g 5313 fvtp3g 5314 fvtp2 5316 fvtp3 5317 zltlen 8095 nn0lt2 8098 fzofzim 8814 |
Copyright terms: Public domain | W3C validator |