Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > imp32 | Unicode version |
Description: An importation inference. (Contributed by NM, 26-Apr-1994.) |
Ref | Expression |
---|---|
imp3.1 |
Ref | Expression |
---|---|
imp32 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imp3.1 | . . 3 | |
2 | 1 | impd 252 | . 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: imp42 352 impr 377 anasss 397 an13s 562 3expb 1199 reuss2 3407 reupick 3411 po2nr 4294 fvmptt 5587 fliftfund 5776 f1ocnv2d 6053 addclpi 7289 addnidpig 7298 mulnqprl 7530 mulnqpru 7531 ltsubrp 9647 ltaddrp 9648 divgcdcoprm0 12055 infpnlem1 12311 innei 12957 tgcnp 13003 isxmetd 13141 |
Copyright terms: Public domain | W3C validator |