| 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 400 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓 ∧ 𝜒))) |
| 3 | id 19 | . . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
| 4 | 3 | anasss 399 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → ((𝜑 ∧ 𝜓) ∧ 𝜒)) |
| 5 | 2, 4 | impbii 126 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) |
| Colors of variables: wff set class |
| Syntax hints: ∧ wa 104 ↔ wb 105 |
| 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 |
| This theorem is referenced by: bianass 469 mpan10 474 an12 561 an32 562 an13 563 an31 564 an4 586 3anass 985 sbidm 1874 4exdistr 1940 2sb5 2011 2sb5rf 2017 sbel2x 2026 r2exf 2524 r19.41 2661 ceqsex3v 2815 ceqsrex2v 2905 rexrab 2936 rexrab2 2940 rexss 3260 inass 3383 difin2 3435 difrab 3447 reupick3 3458 inssdif0im 3528 rexdifpr 3661 rexdifsn 3765 unidif0 4211 bnd2 4217 eqvinop 4287 copsexg 4288 uniuni 4498 rabxp 4712 elvvv 4738 rexiunxp 4820 resopab2 5006 ssrnres 5125 elxp4 5170 elxp5 5171 cnvresima 5172 mptpreima 5176 coass 5201 dff1o2 5527 eqfnfv3 5679 rexsupp 5704 isoini 5887 f1oiso 5895 oprabid 5976 dfoprab2 5992 mpoeq123 6004 mpomptx 6036 resoprab2 6042 ovi3 6083 oprabex3 6214 spc2ed 6319 f1od2 6321 brtpos2 6337 mapsnen 6903 xpsnen 6916 xpcomco 6921 xpassen 6925 ltexpi 7450 enq0enq 7544 enq0tr 7547 prnmaxl 7601 prnminu 7602 genpdflem 7620 ltexprlemm 7713 suplocsrlemb 7919 axaddf 7981 axmulf 7982 rexuz 9701 rexuz2 9702 rexrp 9798 elixx3g 10023 elfz2 10137 fzdifsuc 10203 fzind2 10368 divalgb 12236 gcdass 12336 nnwosdc 12360 lcmass 12407 isprm2 12439 infpn2 12827 fngsum 13220 igsumvalx 13221 issubg3 13528 dfrhm2 13916 ntreq0 14604 tx1cn 14741 tx2cn 14742 blres 14906 metrest 14978 elcncf1di 15051 dedekindicclemicc 15104 fsumdvdsmul 15463 lgsquadlem1 15554 lgsquadlem2 15555 |
| Copyright terms: Public domain | W3C validator |