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 123 | . 2 |
3 | 2 | imp 123 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 |
This theorem is referenced by: imp41 350 imp5d 356 impl 377 anassrs 397 an31s 559 con4biddc 842 3imp 1175 3expa 1181 bilukdc 1374 reusv3 4376 dfimafn 5463 funimass4 5465 funimass3 5529 isopolem 5716 smores2 6184 tfrlem9 6209 nnmordi 6405 mulcanpig 7136 elnnz 9057 nzadd 9099 irradd 9431 irrmul 9432 uzsubsubfz 9820 fzo1fzo0n0 9953 elfzonelfzo 10000 tgcl 12222 |
Copyright terms: Public domain | W3C validator |