![]() |
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 982 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | anass 401 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | bitri 184 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 982 |
This theorem is referenced by: 3anrot 985 3anan12 992 anandi3 993 3exdistr 1927 r3al 2534 ceqsex2 2792 ceqsex3v 2794 ceqsex4v 2795 ceqsex6v 2796 ceqsex8v 2797 eldifpr 3634 rexdifpr 3635 trel3 4124 sowlin 4338 dff1o4 5488 mpoxopovel 6267 dfsmo2 6313 ecopovtrn 6659 ecopovtrng 6662 elixp2 6729 elixp 6732 mptelixpg 6761 eqinfti 7050 distrnqg 7417 recmulnqg 7421 ltexnqq 7438 enq0tr 7464 distrnq0 7489 genpdflem 7537 distrlem1prl 7612 distrlem1pru 7613 divmulasscomap 8684 muldivdirap 8695 divmuldivap 8700 prime 9383 eluz2 9565 raluz2 9611 elixx1 9929 elixx3g 9933 elioo2 9953 elioo5 9965 elicc4 9972 iccneg 10021 icoshft 10022 elfz1 10045 elfz 10046 elfz2 10047 elfzm11 10123 elfz2nn0 10144 elfzo2 10182 elfzo3 10195 lbfzo0 10213 fzind2 10271 zmodid2 10385 redivap 10918 imdivap 10925 maxleast 11257 cosmul 11788 dfgcd2 12050 lcmneg 12109 coprmgcdb 12123 divgcdcoprmex 12137 cncongr1 12138 cncongr2 12139 difsqpwdvds 12373 elgz 12406 xpsfrnel 12823 xpsfrnel2 12825 mgmsscl 12840 ismhm 12928 mhmpropd 12933 issubm 12939 issubg 13129 eqglact 13181 eqgid 13182 ecqusaddd 13194 ecqusaddcl 13195 isrng 13305 issrg 13336 srglmhm 13364 srgrmhm 13365 isring 13371 dfrhm2 13521 issubrng 13563 issubrg3 13611 islmod 13624 islssm 13690 islssmg 13691 lsspropdg 13764 qusmulrng 13863 lmbrf 14192 uptx 14251 txcn 14252 xmetec 14414 bl2ioo 14519 lgsmodeq 14924 lgsmulsqcoprm 14925 findset 15175 |
Copyright terms: Public domain | W3C validator |