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 2166 | . 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) | |
2 | 1 | necon3bii 2372 | 1 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ≠ wne 2334 |
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 1434 ax-gen 1436 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-cleq 2157 df-ne 2335 |
This theorem is referenced by: necomi 2419 necomd 2420 difprsn1 3707 difprsn2 3708 diftpsn3 3709 fndmdifcom 5586 fvpr1 5684 fvpr2 5685 fvpr1g 5686 fvtp1g 5688 fvtp2g 5689 fvtp3g 5690 fvtp2 5692 fvtp3 5693 zltlen 9261 nn0lt2 9264 qltlen 9570 fzofzim 10114 flqeqceilz 10244 isprm2lem 12037 prm2orodd 12047 tridceq 13797 |
Copyright terms: Public domain | W3C validator |