![]() |
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 123 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | com12 30 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 |
This theorem is referenced by: impcomd 253 imp32 255 pm3.31 260 syland 289 imp4c 346 imp4d 347 imp5d 354 expimpd 358 expl 373 pm3.37 661 pm5.6r 893 3expib 1165 sbiedh 1741 equs5 1781 moexexdc 2057 rsp2 2454 moi 2834 reu6 2840 sbciegft 2905 prel12 3662 opthpr 3663 invdisj 3887 sowlin 4200 reusv1 4337 relop 4647 elres 4811 iss 4821 funssres 5121 fv3 5396 funfvima 5601 poxp 6081 tfri3 6216 nndi 6334 nnmass 6335 nnmordi 6364 nnmord 6365 eroveu 6472 fiintim 6768 suplubti 6837 addnq0mo 7197 mulnq0mo 7198 prcdnql 7234 prcunqu 7235 prnmaxl 7238 prnminu 7239 genprndl 7271 genprndu 7272 distrlem1prl 7332 distrlem1pru 7333 distrlem5prl 7336 distrlem5pru 7337 recexprlemss1l 7385 recexprlemss1u 7386 addsrmo 7480 mulsrmo 7481 mulgt0sr 7514 ltleletr 7763 mulgt1 8525 fzind 9064 eqreznegel 9302 fzen 9710 elfzodifsumelfzo 9865 bernneq 10299 mulcn2 10967 divalglemeunn 11460 divalglemeuneg 11462 ndvdssub 11469 algcvgblem 11570 coprmdvds 11613 coprmdvds2 11614 divgcdcoprm0 11622 lmss 12251 lmtopcnp 12255 bj-sbimedh 12662 bj-nnen2lp 12835 |
Copyright terms: Public domain | W3C validator |