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 964 | . 2 | |
2 | anass 398 | . 2 | |
3 | 1, 2 | bitri 183 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 w3a 962 |
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 964 |
This theorem is referenced by: 3anrot 967 3anan12 974 anandi3 975 3exdistr 1887 r3al 2475 ceqsex2 2721 ceqsex3v 2723 ceqsex4v 2724 ceqsex6v 2725 ceqsex8v 2726 trel3 4029 sowlin 4237 dff1o4 5368 mpoxopovel 6131 dfsmo2 6177 ecopovtrn 6519 ecopovtrng 6522 elixp2 6589 elixp 6592 mptelixpg 6621 eqinfti 6900 distrnqg 7188 recmulnqg 7192 ltexnqq 7209 enq0tr 7235 distrnq0 7260 genpdflem 7308 distrlem1prl 7383 distrlem1pru 7384 divmulasscomap 8449 muldivdirap 8460 divmuldivap 8465 prime 9143 eluz2 9325 raluz2 9367 elixx1 9673 elixx3g 9677 elioo2 9697 elioo5 9709 elicc4 9716 iccneg 9765 icoshft 9766 elfz1 9788 elfz 9789 elfz2 9790 elfzm11 9864 elfz2nn0 9885 elfzo2 9920 elfzo3 9933 lbfzo0 9951 fzind2 10009 zmodid2 10118 redivap 10639 imdivap 10646 maxleast 10978 cosmul 11441 dfgcd2 11691 lcmneg 11744 coprmgcdb 11758 divgcdcoprmex 11772 cncongr1 11773 cncongr2 11774 lmbrf 12373 uptx 12432 txcn 12433 xmetec 12595 bl2ioo 12700 findset 13132 |
Copyright terms: Public domain | W3C validator |