![]() |
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 393 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓 ∧ 𝜒))) |
3 | id 19 | . . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
4 | 3 | anasss 392 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → ((𝜑 ∧ 𝜓) ∧ 𝜒)) |
5 | 2, 4 | impbii 125 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: mpan10 459 an12 529 an32 530 an13 531 an31 532 an4 554 3anass 931 sbidm 1786 4exdistr 1848 2sb5 1914 2sb5rf 1920 sbel2x 1929 r2exf 2407 r19.41 2536 ceqsex3v 2675 ceqsrex2v 2763 rexrab 2792 rexrab2 2796 rexss 3103 inass 3225 difin2 3277 difrab 3289 reupick3 3300 inssdif0im 3369 rexdifsn 3594 unidif0 4023 bnd2 4029 eqvinop 4094 copsexg 4095 uniuni 4301 rabxp 4504 elvvv 4530 rexiunxp 4609 resopab2 4792 ssrnres 4907 elxp4 4952 elxp5 4953 cnvresima 4954 mptpreima 4958 coass 4983 dff1o2 5293 eqfnfv3 5438 rexsupp 5462 isoini 5635 f1oiso 5643 oprabid 5719 dfoprab2 5734 mpt2eq123 5746 mpt2mptx 5777 resoprab2 5780 ovi3 5819 oprabex3 5938 spc2ed 6036 f1od2 6038 brtpos2 6054 mapsnen 6608 xpsnen 6617 xpcomco 6622 xpassen 6626 ltexpi 6993 enq0enq 7087 enq0tr 7090 prnmaxl 7144 prnminu 7145 genpdflem 7163 ltexprlemm 7256 rexuz 9167 rexuz2 9168 rexrp 9255 elixx3g 9467 elfz2 9580 fzdifsuc 9644 fzind2 9799 divalgb 11352 gcdass 11431 lcmass 11494 isprm2 11526 ntreq0 11984 blres 12220 metrest 12292 elcncf1di 12332 |
Copyright terms: Public domain | W3C validator |