Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > neeq1d | Unicode version |
Description: Deduction for inequality. (Contributed by NM, 25-Oct-1999.) |
Ref | Expression |
---|---|
neeq1d.1 |
Ref | Expression |
---|---|
neeq1d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neeq1d.1 | . 2 | |
2 | neeq1 2353 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wceq 1348 wne 2340 |
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 609 ax-in2 610 ax-5 1440 ax-gen 1442 ax-4 1503 ax-17 1519 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-cleq 2163 df-ne 2341 |
This theorem is referenced by: neeq12d 2360 eqnetrd 2364 prnzg 3705 hashprg 10730 algcvg 11989 algcvga 11992 eucalgcvga 11999 rpdvds 12040 phibndlem 12157 dfphi2 12161 pcaddlem 12279 ennnfoneleminc 12353 ennnfonelemex 12356 ennnfonelemhom 12357 ennnfonelemnn0 12364 ennnfonelemr 12365 ennnfonelemim 12366 ctinfomlemom 12369 lgsne0 13654 dceqnconst 14013 dcapnconst 14014 nconstwlpolem 14018 |
Copyright terms: Public domain | W3C validator |