![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > imp31 | Unicode version |
Description: An importation inference. (Contributed by NM, 26-Apr-1994.) |
Ref | Expression |
---|---|
imp3.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
imp31 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imp3.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | imp 124 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | imp 124 |
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 |
This theorem is referenced by: imp41 353 imp5d 359 impl 380 anassrs 400 an31s 570 con4biddc 857 3imp 1193 3expa 1203 bilukdc 1396 reusv3 4460 dfimafn 5564 funimass4 5566 funimass3 5632 isopolem 5822 smores2 6294 tfrlem9 6319 nnmordi 6516 mulcanpig 7333 elnnz 9262 nzadd 9304 irradd 9645 irrmul 9646 uzsubsubfz 10046 fzo1fzo0n0 10182 elfzonelfzo 10229 infpnlem1 12356 tgcl 13534 |
Copyright terms: Public domain | W3C validator |