![]() |
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 984 sbidm 1862 4exdistr 1928 2sb5 1995 2sb5rf 2001 sbel2x 2010 r2exf 2508 r19.41 2645 ceqsex3v 2794 ceqsrex2v 2884 rexrab 2915 rexrab2 2919 rexss 3237 inass 3360 difin2 3412 difrab 3424 reupick3 3435 inssdif0im 3505 rexdifpr 3638 rexdifsn 3742 unidif0 4188 bnd2 4194 eqvinop 4264 copsexg 4265 uniuni 4472 rabxp 4684 elvvv 4710 rexiunxp 4790 resopab2 4975 ssrnres 5092 elxp4 5137 elxp5 5138 cnvresima 5139 mptpreima 5143 coass 5168 dff1o2 5488 eqfnfv3 5639 rexsupp 5664 isoini 5843 f1oiso 5851 oprabid 5932 dfoprab2 5947 mpoeq123 5959 mpomptx 5991 resoprab2 5997 ovi3 6037 oprabex3 6158 spc2ed 6262 f1od2 6264 brtpos2 6280 mapsnen 6841 xpsnen 6851 xpcomco 6856 xpassen 6860 ltexpi 7371 enq0enq 7465 enq0tr 7468 prnmaxl 7522 prnminu 7523 genpdflem 7541 ltexprlemm 7634 suplocsrlemb 7840 axaddf 7902 axmulf 7903 rexuz 9616 rexuz2 9617 rexrp 9712 elixx3g 9937 elfz2 10051 fzdifsuc 10117 fzind2 10275 divalgb 11971 gcdass 12057 nnwosdc 12081 lcmass 12128 isprm2 12160 infpn2 12518 fngsum 12875 igsumvalx 12876 issubg3 13156 dfrhm2 13529 ntreq0 14117 tx1cn 14254 tx2cn 14255 blres 14419 metrest 14491 elcncf1di 14551 dedekindicclemicc 14595 |
Copyright terms: Public domain | W3C validator |