![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > neii | Unicode version |
Description: Inference associated with df-ne 2348. (Contributed by BJ, 7-Jul-2018.) |
Ref | Expression |
---|---|
neii.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
neii |
![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neii.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | df-ne 2348 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpbi 145 |
1
![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 |
This theorem depends on definitions: df-bi 117 df-ne 2348 |
This theorem is referenced by: 2dom 6798 updjudhcoinrg 7073 omp1eomlem 7086 nninfisol 7124 exmidomni 7133 mkvprop 7149 nninfwlporlemd 7163 nninfwlpoimlemginf 7167 exmidfodomrlemr 7194 exmidfodomrlemrALT 7195 exmidaclem 7200 ine0 8328 inelr 8518 xrltnr 9753 pnfnlt 9761 xrlttri3 9771 nltpnft 9788 xrpnfdc 9816 xrmnfdc 9817 xleaddadd 9861 zfz1iso 10792 3lcm2e6woprm 12056 6lcm4e12 12057 m1dvdsndvds 12218 unct 12413 bj-charfunbi 14185 pwle2 14370 subctctexmid 14373 pw1nct 14375 peano3nninf 14379 nninfsellemqall 14387 nninffeq 14392 |
Copyright terms: Public domain | W3C validator |