Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3anass | Unicode version |
Description: Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.) |
Ref | Expression |
---|---|
3anass |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3an 949 | . 2 | |
2 | anass 398 | . 2 | |
3 | 1, 2 | bitri 183 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 w3a 947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 949 |
This theorem is referenced by: 3anrot 952 3anan12 959 anandi3 960 3exdistr 1869 r3al 2454 ceqsex2 2700 ceqsex3v 2702 ceqsex4v 2703 ceqsex6v 2704 ceqsex8v 2705 trel3 4004 sowlin 4212 dff1o4 5343 mpoxopovel 6106 dfsmo2 6152 ecopovtrn 6494 ecopovtrng 6497 elixp2 6564 elixp 6567 mptelixpg 6596 eqinfti 6875 distrnqg 7163 recmulnqg 7167 ltexnqq 7184 enq0tr 7210 distrnq0 7235 genpdflem 7283 distrlem1prl 7358 distrlem1pru 7359 divmulasscomap 8423 muldivdirap 8434 divmuldivap 8439 prime 9108 eluz2 9288 raluz2 9330 elixx1 9635 elixx3g 9639 elioo2 9659 elioo5 9671 elicc4 9678 iccneg 9727 icoshft 9728 elfz1 9750 elfz 9751 elfz2 9752 elfzm11 9826 elfz2nn0 9847 elfzo2 9882 elfzo3 9895 lbfzo0 9913 fzind2 9971 zmodid2 10080 redivap 10601 imdivap 10608 maxleast 10940 cosmul 11366 dfgcd2 11614 lcmneg 11667 coprmgcdb 11681 divgcdcoprmex 11695 cncongr1 11696 cncongr2 11697 lmbrf 12295 uptx 12354 txcn 12355 xmetec 12517 bl2ioo 12622 findset 13039 |
Copyright terms: Public domain | W3C validator |