Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > neii | GIF version |
Description: Inference associated with df-ne 2309. (Contributed by BJ, 7-Jul-2018.) |
Ref | Expression |
---|---|
neii.1 | ⊢ 𝐴 ≠ 𝐵 |
Ref | Expression |
---|---|
neii | ⊢ ¬ 𝐴 = 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neii.1 | . 2 ⊢ 𝐴 ≠ 𝐵 | |
2 | df-ne 2309 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
3 | 1, 2 | mpbi 144 | 1 ⊢ ¬ 𝐴 = 𝐵 |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 = wceq 1331 ≠ wne 2308 |
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 2309 |
This theorem is referenced by: 2dom 6699 updjudhcoinrg 6966 omp1eomlem 6979 exmidomni 7014 mkvprop 7032 exmidfodomrlemr 7058 exmidfodomrlemrALT 7059 exmidaclem 7064 ine0 8156 inelr 8346 xrltnr 9566 pnfnlt 9573 xrlttri3 9583 nltpnft 9597 xrpnfdc 9625 xrmnfdc 9626 xleaddadd 9670 zfz1iso 10584 3lcm2e6woprm 11767 6lcm4e12 11768 unct 11954 pwle2 13193 subctctexmid 13196 peano3nninf 13201 nninfsellemqall 13211 nninffeq 13216 |
Copyright terms: Public domain | W3C validator |