Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > necomd | GIF version |
Description: Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.) |
Ref | Expression |
---|---|
necomd.1 | ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
Ref | Expression |
---|---|
necomd | ⊢ (𝜑 → 𝐵 ≠ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necomd.1 | . 2 ⊢ (𝜑 → 𝐴 ≠ 𝐵) | |
2 | necom 2418 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴) | |
3 | 1, 2 | sylib 121 | 1 ⊢ (𝜑 → 𝐵 ≠ 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ≠ 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: difsnb 3710 0nelop 4220 frecabcl 6358 fidifsnen 6827 tpfidisj 6884 omp1eomlem 7050 difinfsnlem 7055 fodjuomnilemdc 7099 en2eleq 7142 en2other2 7143 ltned 8003 lt0ne0 8317 zdceq 9257 zneo 9283 xrlttri3 9724 qdceq 10172 flqltnz 10212 nn0opthd 10624 hashdifpr 10722 sumtp 11341 isprm2lem 12027 oddprm 12170 pcmpt 12252 ennnfonelemex 12290 |
Copyright terms: Public domain | W3C validator |