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 969 | . 2 | |
2 | anass 399 | . 2 | |
3 | 1, 2 | bitri 183 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 w3a 967 |
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 969 |
This theorem is referenced by: 3anrot 972 3anan12 979 anandi3 980 3exdistr 1902 r3al 2508 ceqsex2 2761 ceqsex3v 2763 ceqsex4v 2764 ceqsex6v 2765 ceqsex8v 2766 eldifpr 3597 rexdifpr 3598 trel3 4082 sowlin 4292 dff1o4 5434 mpoxopovel 6200 dfsmo2 6246 ecopovtrn 6589 ecopovtrng 6592 elixp2 6659 elixp 6662 mptelixpg 6691 eqinfti 6976 distrnqg 7319 recmulnqg 7323 ltexnqq 7340 enq0tr 7366 distrnq0 7391 genpdflem 7439 distrlem1prl 7514 distrlem1pru 7515 divmulasscomap 8583 muldivdirap 8594 divmuldivap 8599 prime 9281 eluz2 9463 raluz2 9508 elixx1 9824 elixx3g 9828 elioo2 9848 elioo5 9860 elicc4 9867 iccneg 9916 icoshft 9917 elfz1 9940 elfz 9941 elfz2 9942 elfzm11 10016 elfz2nn0 10037 elfzo2 10075 elfzo3 10088 lbfzo0 10106 fzind2 10164 zmodid2 10277 redivap 10802 imdivap 10809 maxleast 11141 cosmul 11672 dfgcd2 11932 lcmneg 11985 coprmgcdb 11999 divgcdcoprmex 12013 cncongr1 12014 cncongr2 12015 difsqpwdvds 12248 lmbrf 12762 uptx 12821 txcn 12822 xmetec 12984 bl2ioo 13089 findset 13668 |
Copyright terms: Public domain | W3C validator |