![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3anass | GIF version |
Description: Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.) |
Ref | Expression |
---|---|
3anass | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3an 980 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
2 | anass 401 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) | |
3 | 1, 2 | bitri 184 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 104 ↔ wb 105 ∧ w3a 978 |
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 980 |
This theorem is referenced by: 3anrot 983 3anan12 990 anandi3 991 3exdistr 1915 r3al 2521 ceqsex2 2777 ceqsex3v 2779 ceqsex4v 2780 ceqsex6v 2781 ceqsex8v 2782 eldifpr 3619 rexdifpr 3620 trel3 4107 sowlin 4318 dff1o4 5466 mpoxopovel 6237 dfsmo2 6283 ecopovtrn 6627 ecopovtrng 6630 elixp2 6697 elixp 6700 mptelixpg 6729 eqinfti 7014 distrnqg 7381 recmulnqg 7385 ltexnqq 7402 enq0tr 7428 distrnq0 7453 genpdflem 7501 distrlem1prl 7576 distrlem1pru 7577 divmulasscomap 8647 muldivdirap 8658 divmuldivap 8663 prime 9346 eluz2 9528 raluz2 9573 elixx1 9891 elixx3g 9895 elioo2 9915 elioo5 9927 elicc4 9934 iccneg 9983 icoshft 9984 elfz1 10007 elfz 10008 elfz2 10009 elfzm11 10084 elfz2nn0 10105 elfzo2 10143 elfzo3 10156 lbfzo0 10174 fzind2 10232 zmodid2 10345 redivap 10874 imdivap 10881 maxleast 11213 cosmul 11744 dfgcd2 12005 lcmneg 12064 coprmgcdb 12078 divgcdcoprmex 12092 cncongr1 12093 cncongr2 12094 difsqpwdvds 12327 elgz 12359 mgmsscl 12710 ismhm 12781 mhmpropd 12785 issubm 12791 issubg 12960 issrg 13048 srglmhm 13076 srgrmhm 13077 isring 13083 lmbrf 13497 uptx 13556 txcn 13557 xmetec 13719 bl2ioo 13824 lgsmodeq 14228 lgsmulsqcoprm 14229 findset 14468 |
Copyright terms: Public domain | W3C validator |