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 2319 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wceq 1331 wne 2306 |
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 603 ax-in2 604 ax-5 1423 ax-gen 1425 ax-4 1487 ax-17 1506 ax-ext 2119 |
This theorem depends on definitions: df-bi 116 df-cleq 2130 df-ne 2307 |
This theorem is referenced by: neeq12d 2326 eqnetrd 2330 prnzg 3642 hashprg 10547 algcvg 11718 algcvga 11721 eucalgcvga 11728 rpdvds 11769 phibndlem 11881 dfphi2 11885 ennnfoneleminc 11913 ennnfonelemex 11916 ennnfonelemhom 11917 ennnfonelemnn0 11924 ennnfonelemr 11925 ennnfonelemim 11926 ctinfomlemom 11929 |
Copyright terms: Public domain | W3C validator |