![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3expb | Unicode version |
Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) |
Ref | Expression |
---|---|
3exp.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3expb |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3exp 1142 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | imp32 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 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 926 |
This theorem is referenced by: 3adant3r1 1152 3adant3r2 1153 3adant3r3 1154 3adant1l 1166 3adant1r 1167 mp3an1 1260 soinxp 4508 sotri 4827 fnfco 5185 mpt2eq3dva 5713 fovrnda 5788 ovelrn 5793 grprinvd 5840 nnmsucr 6249 fidifsnid 6587 exmidpw 6624 undiffi 6635 fidcenumlemim 6661 ltpopr 7154 ltexprlemdisj 7165 recexprlemdisj 7189 mul4 7614 add4 7643 2addsub 7696 addsubeq4 7697 subadd4 7726 muladd 7862 ltleadd 7924 divmulap 8142 divap0 8151 div23ap 8158 div12ap 8161 divsubdirap 8175 divcanap5 8181 divmuleqap 8184 divcanap6 8186 divdiv32ap 8187 div2subap 8302 letrp1 8309 lemul12b 8322 lediv1 8330 cju 8421 nndivre 8458 nndivtr 8464 nn0addge1 8719 nn0addge2 8720 peano2uz2 8853 uzind 8857 uzind3 8859 fzind 8861 fnn0ind 8862 uzind4 9076 qre 9110 irrmul 9132 rpdivcl 9159 rerpdivcl 9164 iccshftr 9411 iccshftl 9413 iccdil 9415 icccntr 9417 fzaddel 9473 fzrev 9498 frec2uzf1od 9813 expdivap 10006 2shfti 10265 iisermulc2 10728 dvds2add 11108 dvds2sub 11109 dvdstr 11111 alzdvds 11133 divalg2 11204 lcmgcdlem 11337 lcmgcdeq 11343 isprm6 11404 cncffvrn 11638 divccncfap 11646 |
Copyright terms: Public domain | W3C validator |