![]() |
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 254 |
. 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: imp42 354 impr 379 anasss 399 an13s 567 3expb 1204 reuss2 3415 reupick 3419 po2nr 4309 fvmptt 5607 fliftfund 5797 f1ocnv2d 6074 addclpi 7325 addnidpig 7334 mulnqprl 7566 mulnqpru 7567 ltsubrp 9688 ltaddrp 9689 divgcdcoprm0 12095 infpnlem1 12351 innei 13594 tgcnp 13640 isxmetd 13778 |
Copyright terms: Public domain | W3C validator |