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 75 | . . 3 |
3 | 2 | imp 115 | . 2 |
4 | 3 | com12 27 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 |
This theorem is referenced by: imp32 244 pm3.31 249 syland 277 imp4c 333 imp4d 334 imp5d 341 expimpd 345 expl 360 pm5.6r 836 3expib 1107 sbiedh 1670 equs5 1710 moexexdc 1984 rsp2 2371 moi 2724 reu6 2730 sbciegft 2793 prel12 3542 opthpr 3543 invdisj 3759 sowlin 4057 reusv1 4190 relop 4486 elres 4646 iss 4654 funssres 4942 fv3 5197 funfvima 5390 poxp 5853 tfri3 5953 nndi 6065 nnmass 6066 nnmordi 6089 nnmord 6090 eroveu 6197 addnq0mo 6545 mulnq0mo 6546 prcdnql 6582 prcunqu 6583 prnmaxl 6586 prnminu 6587 genprndl 6619 genprndu 6620 distrlem1prl 6680 distrlem1pru 6681 distrlem5prl 6684 distrlem5pru 6685 recexprlemss1l 6733 recexprlemss1u 6734 addsrmo 6828 mulsrmo 6829 mulgt0sr 6862 ltleletr 7100 mulgt1 7829 fzind 8353 eqreznegel 8549 fzen 8907 elfzodifsumelfzo 9057 bernneq 9369 mulcn2 9833 algcvgblem 9888 bj-sbimedh 9911 bj-nnen2lp 10079 |
Copyright terms: Public domain | W3C validator |