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 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 2477 ceqsex2 2726 ceqsex3v 2728 ceqsex4v 2729 ceqsex6v 2730 ceqsex8v 2731 trel3 4034 sowlin 4242 dff1o4 5375 mpoxopovel 6138 dfsmo2 6184 ecopovtrn 6526 ecopovtrng 6529 elixp2 6596 elixp 6599 mptelixpg 6628 eqinfti 6907 distrnqg 7195 recmulnqg 7199 ltexnqq 7216 enq0tr 7242 distrnq0 7267 genpdflem 7315 distrlem1prl 7390 distrlem1pru 7391 divmulasscomap 8456 muldivdirap 8467 divmuldivap 8472 prime 9150 eluz2 9332 raluz2 9374 elixx1 9680 elixx3g 9684 elioo2 9704 elioo5 9716 elicc4 9723 iccneg 9772 icoshft 9773 elfz1 9795 elfz 9796 elfz2 9797 elfzm11 9871 elfz2nn0 9892 elfzo2 9927 elfzo3 9940 lbfzo0 9958 fzind2 10016 zmodid2 10125 redivap 10646 imdivap 10653 maxleast 10985 cosmul 11452 dfgcd2 11702 lcmneg 11755 coprmgcdb 11769 divgcdcoprmex 11783 cncongr1 11784 cncongr2 11785 lmbrf 12384 uptx 12443 txcn 12444 xmetec 12606 bl2ioo 12711 findset 13143 |
Copyright terms: Public domain | W3C validator |