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 397 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓 ∧ 𝜒))) |
3 | id 19 | . . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
4 | 3 | anasss 396 | . 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-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: mpan10 465 an12 550 an32 551 an13 552 an31 553 an4 575 3anass 966 sbidm 1823 4exdistr 1888 2sb5 1958 2sb5rf 1964 sbel2x 1973 r2exf 2453 r19.41 2586 ceqsex3v 2728 ceqsrex2v 2817 rexrab 2847 rexrab2 2851 rexss 3164 inass 3286 difin2 3338 difrab 3350 reupick3 3361 inssdif0im 3430 rexdifsn 3655 unidif0 4091 bnd2 4097 eqvinop 4165 copsexg 4166 uniuni 4372 rabxp 4576 elvvv 4602 rexiunxp 4681 resopab2 4866 ssrnres 4981 elxp4 5026 elxp5 5027 cnvresima 5028 mptpreima 5032 coass 5057 dff1o2 5372 eqfnfv3 5520 rexsupp 5544 isoini 5719 f1oiso 5727 oprabid 5803 dfoprab2 5818 mpoeq123 5830 mpomptx 5862 resoprab2 5868 ovi3 5907 oprabex3 6027 spc2ed 6130 f1od2 6132 brtpos2 6148 mapsnen 6705 xpsnen 6715 xpcomco 6720 xpassen 6724 ltexpi 7145 enq0enq 7239 enq0tr 7242 prnmaxl 7296 prnminu 7297 genpdflem 7315 ltexprlemm 7408 suplocsrlemb 7614 axaddf 7676 axmulf 7677 rexuz 9375 rexuz2 9376 rexrp 9464 elixx3g 9684 elfz2 9797 fzdifsuc 9861 fzind2 10016 divalgb 11622 gcdass 11703 lcmass 11766 isprm2 11798 ntreq0 12301 tx1cn 12438 tx2cn 12439 blres 12603 metrest 12675 elcncf1di 12735 dedekindicclemicc 12779 |
Copyright terms: Public domain | W3C validator |