![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nesymi | Unicode version |
Description: Inference associated with nesym 2404. (Contributed by BJ, 7-Jul-2018.) |
Ref | Expression |
---|---|
nesymi.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nesymi |
![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nesymi.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | nesym 2404 |
. 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 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-5 1457 ax-gen 1459 ax-ext 2170 |
This theorem depends on definitions: df-bi 117 df-cleq 2181 df-ne 2360 |
This theorem is referenced by: frec0g 6415 djune 7094 omp1eomlem 7110 fodjum 7161 fodju0 7162 ismkvnex 7170 mkvprop 7173 omniwomnimkv 7182 3nelsucpw1 7250 xrltnr 9796 nltmnf 9805 xnn0xadd0 9884 fnpr2ob 12781 pwle2 15132 nninfalllem1 15141 nninfall 15142 nninfsellemeq 15147 trirec0xor 15177 |
Copyright terms: Public domain | W3C validator |