![]() |
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 947 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | anass 396 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | bitri 183 |
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 947 |
This theorem is referenced by: 3anrot 950 3anan12 957 anandi3 958 3exdistr 1867 r3al 2451 ceqsex2 2697 ceqsex3v 2699 ceqsex4v 2700 ceqsex6v 2701 ceqsex8v 2702 trel3 3994 sowlin 4202 dff1o4 5331 mpoxopovel 6092 dfsmo2 6138 ecopovtrn 6480 ecopovtrng 6483 elixp2 6550 elixp 6553 mptelixpg 6582 eqinfti 6859 distrnqg 7143 recmulnqg 7147 ltexnqq 7164 enq0tr 7190 distrnq0 7215 genpdflem 7263 distrlem1prl 7338 distrlem1pru 7339 divmulasscomap 8369 muldivdirap 8380 divmuldivap 8385 prime 9054 eluz2 9234 raluz2 9276 elixx1 9573 elixx3g 9577 elioo2 9597 elioo5 9609 elicc4 9616 iccneg 9665 icoshft 9666 elfz1 9688 elfz 9689 elfz2 9690 elfzm11 9764 elfz2nn0 9785 elfzo2 9820 elfzo3 9833 lbfzo0 9851 fzind2 9909 zmodid2 10018 redivap 10539 imdivap 10546 maxleast 10877 cosmul 11303 dfgcd2 11548 lcmneg 11601 coprmgcdb 11615 divgcdcoprmex 11629 cncongr1 11630 cncongr2 11631 lmbrf 12226 uptx 12285 txcn 12286 xmetec 12426 bl2ioo 12528 findset 12835 |
Copyright terms: Public domain | W3C validator |