![]() |
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 982 sbidm 1851 4exdistr 1916 2sb5 1983 2sb5rf 1989 sbel2x 1998 r2exf 2495 r19.41 2632 ceqsex3v 2780 ceqsrex2v 2870 rexrab 2901 rexrab2 2905 rexss 3223 inass 3346 difin2 3398 difrab 3410 reupick3 3421 inssdif0im 3491 rexdifpr 3621 rexdifsn 3725 unidif0 4168 bnd2 4174 eqvinop 4244 copsexg 4245 uniuni 4452 rabxp 4664 elvvv 4690 rexiunxp 4770 resopab2 4955 ssrnres 5072 elxp4 5117 elxp5 5118 cnvresima 5119 mptpreima 5123 coass 5148 dff1o2 5467 eqfnfv3 5616 rexsupp 5641 isoini 5819 f1oiso 5827 oprabid 5907 dfoprab2 5922 mpoeq123 5934 mpomptx 5966 resoprab2 5972 ovi3 6011 oprabex3 6130 spc2ed 6234 f1od2 6236 brtpos2 6252 mapsnen 6811 xpsnen 6821 xpcomco 6826 xpassen 6830 ltexpi 7336 enq0enq 7430 enq0tr 7433 prnmaxl 7487 prnminu 7488 genpdflem 7506 ltexprlemm 7599 suplocsrlemb 7805 axaddf 7867 axmulf 7868 rexuz 9580 rexuz2 9581 rexrp 9676 elixx3g 9901 elfz2 10015 fzdifsuc 10081 fzind2 10239 divalgb 11930 gcdass 12016 nnwosdc 12040 lcmass 12085 isprm2 12117 infpn2 12457 issubg3 13052 ntreq0 13635 tx1cn 13772 tx2cn 13773 blres 13937 metrest 14009 elcncf1di 14069 dedekindicclemicc 14113 |
Copyright terms: Public domain | W3C validator |