![]() |
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 2373 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
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 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-5 1458 ax-gen 1460 ax-4 1521 ax-17 1537 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-cleq 2182 df-ne 2361 |
This theorem is referenced by: neeq12d 2380 eqnetrd 2384 prnzg 3731 pw2f1odclem 6862 hashprg 10820 algcvg 12080 algcvga 12083 eucalgcvga 12090 rpdvds 12131 phibndlem 12248 dfphi2 12252 pcaddlem 12371 ennnfoneleminc 12462 ennnfonelemex 12465 ennnfonelemhom 12466 ennnfonelemnn0 12473 ennnfonelemr 12474 ennnfonelemim 12475 ctinfomlemom 12478 setscomd 12553 lgsne0 14897 dceqnconst 15267 dcapnconst 15268 nconstwlpolem 15272 |
Copyright terms: Public domain | W3C validator |