![]() |
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 3618 rexdifpr 3619 trel3 4106 sowlin 4316 dff1o4 5464 mpoxopovel 6235 dfsmo2 6281 ecopovtrn 6625 ecopovtrng 6628 elixp2 6695 elixp 6698 mptelixpg 6727 eqinfti 7012 distrnqg 7364 recmulnqg 7368 ltexnqq 7385 enq0tr 7411 distrnq0 7436 genpdflem 7484 distrlem1prl 7559 distrlem1pru 7560 divmulasscomap 8629 muldivdirap 8640 divmuldivap 8645 prime 9328 eluz2 9510 raluz2 9555 elixx1 9871 elixx3g 9875 elioo2 9895 elioo5 9907 elicc4 9914 iccneg 9963 icoshft 9964 elfz1 9987 elfz 9988 elfz2 9989 elfzm11 10064 elfz2nn0 10085 elfzo2 10123 elfzo3 10136 lbfzo0 10154 fzind2 10212 zmodid2 10325 redivap 10854 imdivap 10861 maxleast 11193 cosmul 11724 dfgcd2 11985 lcmneg 12044 coprmgcdb 12058 divgcdcoprmex 12072 cncongr1 12073 cncongr2 12074 difsqpwdvds 12307 elgz 12339 mgmsscl 12659 ismhm 12730 mhmpropd 12734 issubm 12740 issrg 12961 srglmhm 12989 srgrmhm 12990 isring 12996 lmbrf 13348 uptx 13407 txcn 13408 xmetec 13570 bl2ioo 13675 lgsmodeq 14079 lgsmulsqcoprm 14080 findset 14319 |
Copyright terms: Public domain | W3C validator |