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 557 3expb 1186 reuss2 3387 reupick 3391 po2nr 4269 fvmptt 5559 fliftfund 5747 f1ocnv2d 6024 addclpi 7247 addnidpig 7256 mulnqprl 7488 mulnqpru 7489 ltsubrp 9597 ltaddrp 9598 divgcdcoprm0 11978 innei 12574 tgcnp 12620 isxmetd 12758 |
Copyright terms: Public domain | W3C validator |