Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > neii | GIF version |
Description: Inference associated with df-ne 2286. (Contributed by BJ, 7-Jul-2018.) |
Ref | Expression |
---|---|
neii.1 | ⊢ 𝐴 ≠ 𝐵 |
Ref | Expression |
---|---|
neii | ⊢ ¬ 𝐴 = 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neii.1 | . 2 ⊢ 𝐴 ≠ 𝐵 | |
2 | df-ne 2286 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
3 | 1, 2 | mpbi 144 | 1 ⊢ ¬ 𝐴 = 𝐵 |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 = wceq 1316 ≠ wne 2285 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 df-ne 2286 |
This theorem is referenced by: 2dom 6667 updjudhcoinrg 6934 omp1eomlem 6947 exmidomni 6982 mkvprop 7000 exmidfodomrlemr 7026 exmidfodomrlemrALT 7027 exmidaclem 7032 ine0 8124 inelr 8314 xrltnr 9534 pnfnlt 9541 xrlttri3 9551 nltpnft 9565 xrpnfdc 9593 xrmnfdc 9594 xleaddadd 9638 zfz1iso 10552 3lcm2e6woprm 11694 6lcm4e12 11695 unct 11881 pwle2 13120 subctctexmid 13123 peano3nninf 13128 nninfsellemqall 13138 nninffeq 13143 |
Copyright terms: Public domain | W3C validator |