![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > anass | GIF version |
Description: Associative law for conjunction. Theorem *4.32 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
Ref | Expression |
---|---|
anass | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∧ 𝜒))) | |
2 | 1 | anassrs 392 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓 ∧ 𝜒))) |
3 | id 19 | . . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
4 | 3 | anasss 391 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → ((𝜑 ∧ 𝜓) ∧ 𝜒)) |
5 | 2, 4 | impbii 124 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 102 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: mpan10 458 an12 526 an32 527 an13 528 an31 529 an4 551 3anass 924 sbidm 1773 4exdistr 1835 2sb5 1901 2sb5rf 1907 sbel2x 1916 r2exf 2385 r19.41 2510 ceqsex3v 2642 ceqsrex2v 2728 rexrab 2756 rexrab2 2760 rexss 3062 inass 3177 difin2 3227 difrab 3239 reupick3 3250 inssdif0im 3312 rexdifsn 3523 unidif0 3943 bnd2 3949 eqvinop 4000 copsexg 4001 uniuni 4203 rabxp 4400 elvvv 4423 rexiunxp 4500 resopab2 4679 ssrnres 4787 elxp4 4832 elxp5 4833 cnvresima 4834 mptpreima 4838 coass 4863 dff1o2 5156 eqfnfv3 5293 rexsupp 5317 isoini 5482 f1oiso 5490 oprabid 5562 dfoprab2 5577 mpt2eq123 5589 mpt2mptx 5620 resoprab2 5623 ovi3 5662 oprabex3 5781 spc2ed 5879 f1od2 5881 brtpos2 5894 xpsnen 6355 xpcomco 6360 xpassen 6364 ltexpi 6578 enq0enq 6672 enq0tr 6675 prnmaxl 6729 prnminu 6730 genpdflem 6748 ltexprlemm 6841 rexuz 8738 rexuz2 8739 rexrp 8826 elixx3g 8989 elfz2 9101 fzdifsuc 9163 fzind2 9314 divalgb 10458 gcdass 10537 lcmass 10600 isprm2 10632 |
Copyright terms: Public domain | W3C validator |