| Mathbox for Jonathan Ben-Naim |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > df-bnj17 | Structured version Visualization version GIF version | ||
| Description: Define the 4-way conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| df-bnj17 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wph | . . 3 wff 𝜑 | |
| 2 | wps | . . 3 wff 𝜓 | |
| 3 | wch | . . 3 wff 𝜒 | |
| 4 | wth | . . 3 wff 𝜃 | |
| 5 | 1, 2, 3, 4 | w-bnj17 34884 | . 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) |
| 6 | 1, 2, 3 | w3a 1093 | . . 3 wff (𝜑 ∧ 𝜓 ∧ 𝜒) |
| 7 | 6, 4 | wa 397 | . 2 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) |
| 8 | 5, 7 | wb 208 | 1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) |
| Colors of variables: wff setvar class |
| This definition is referenced by: bnj248 34898 bnj250 34899 bnj258 34906 bnj268 34907 bnj291 34909 bnj312 34910 bnj446 34915 bnj645 34948 bnj658 34949 bnj887 34963 bnj919 34965 bnj945 34971 bnj951 34973 bnj982 34976 bnj1019 34977 bnj518 35083 bnj571 35103 bnj594 35109 bnj916 35130 bnj966 35141 bnj967 35142 bnj1006 35157 bnj1018g 35160 bnj1018 35161 bnj1040 35169 bnj1174 35200 bnj1175 35201 bnj1311 35221 |
| Copyright terms: Public domain | W3C validator |