![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3expa | Unicode version |
Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) |
Ref | Expression |
---|---|
3exp.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3expa |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3exp 1143 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | imp31 253 |
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 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 927 |
This theorem is referenced by: 3anidm23 1234 mp3an2 1262 mpd3an3 1275 rgen3 2461 moi2 2799 sbc3ie 2915 preq12bg 3625 issod 4157 wepo 4197 reuhypd 4308 funimass4 5370 fvtp1g 5521 f1imass 5569 fcof1o 5584 f1ofveu 5656 f1ocnvfv3 5657 acexmid 5667 2ndrn 5969 frecrdg 6189 oawordriexmid 6247 mapxpen 6620 findcard 6660 findcard2 6661 findcard2s 6662 ltapig 6960 ltanqi 7024 ltmnqi 7025 lt2addnq 7026 lt2mulnq 7027 prarloclemcalc 7124 genpassl 7146 genpassu 7147 prmuloc 7188 ltexprlemm 7222 ltexprlemfl 7231 ltexprlemfu 7233 lteupri 7239 ltaprg 7241 mul4 7677 add4 7706 cnegexlem2 7721 cnegexlem3 7722 2addsub 7759 addsubeq4 7760 muladd 7925 ltleadd 7987 reapmul1 8135 apreim 8143 receuap 8201 p1le 8373 lemul12b 8385 lbinf 8472 zdiv 8897 fzind 8924 fnn0ind 8925 uzss 9102 qmulcl 9185 qreccl 9190 xrlttr 9328 icc0r 9407 iooshf 9433 elfz5 9495 elfz0fzfz0 9600 fzind2 9713 ioo0 9734 ico0 9736 ioc0 9737 expnegap0 10026 expineg2 10027 mulexpzap 10058 expsubap 10066 expnbnd 10140 facndiv 10210 bccmpl 10225 ibcval5 10234 bcpasc 10237 crim 10355 climshftlemg 10753 2sumeq2dv 10823 hash2iun 10936 dvdsval3 11141 dvdsnegb 11154 muldvds1 11162 muldvds2 11163 dvdscmul 11164 dvdsmulc 11165 dvds2ln 11170 divalgb 11266 ndvdssub 11271 gcddiv 11349 rpexp1i 11474 phiprmpw 11539 hashgcdeq 11545 innei 11926 |
Copyright terms: Public domain | W3C validator |