![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > impd | Unicode version |
Description: Importation deduction. (Contributed by NM, 31-Mar-1994.) |
Ref | Expression |
---|---|
imp3.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
impd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imp3.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | com3l 81 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | imp 124 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | com12 30 |
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: impcomd 255 imp32 257 pm3.31 262 syland 293 imp4c 351 imp4d 352 imp5d 359 expimpd 363 expl 378 pm3.37 689 pm5.6r 927 3expib 1206 sbiedh 1787 equs5 1829 moexexdc 2110 rsp2 2527 moi 2920 reu6 2926 sbciegft 2993 prel12 3769 opthpr 3770 invdisj 3994 sowlin 4316 reusv1 4454 relop 4772 elres 4938 iss 4948 funssres 5253 fv3 5533 funfvima 5742 poxp 6226 tfri3 6361 nndi 6480 nnmass 6481 nnmordi 6510 nnmord 6511 eroveu 6619 fiintim 6921 suplubti 6992 addnq0mo 7424 mulnq0mo 7425 prcdnql 7461 prcunqu 7462 prnmaxl 7465 prnminu 7466 genprndl 7498 genprndu 7499 distrlem1prl 7559 distrlem1pru 7560 distrlem5prl 7563 distrlem5pru 7564 recexprlemss1l 7612 recexprlemss1u 7613 addsrmo 7720 mulsrmo 7721 mulgt0sr 7755 ltleletr 8016 mulgt1 8796 fzind 9344 eqreznegel 9590 fzen 10016 elfzodifsumelfzo 10174 bernneq 10613 mulcn2 11291 prodmodclem2 11556 dvdsmod0 11771 divalglemeunn 11896 divalglemeuneg 11898 ndvdssub 11905 algcvgblem 12019 coprmdvds 12062 coprmdvds2 12063 divgcdcoprm0 12071 pceu 12265 dvdsprmpweqnn 12305 oddprmdvds 12322 infpnlem1 12327 sgrpidmndm 12700 lmss 13379 lmtopcnp 13383 zabsle1 14033 bj-sbimedh 14145 bj-nnen2lp 14328 |
Copyright terms: Public domain | W3C validator |