| 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 34700 | . 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) |
| 6 | 1, 2, 3 | w3a 1087 | . . 3 wff (𝜑 ∧ 𝜓 ∧ 𝜒) |
| 7 | 6, 4 | wa 395 | . 2 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) |
| 8 | 5, 7 | wb 206 | 1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) |
| Colors of variables: wff setvar class |
| This definition is referenced by: bnj248 34714 bnj250 34715 bnj258 34722 bnj268 34723 bnj291 34725 bnj312 34726 bnj446 34731 bnj645 34764 bnj658 34765 bnj887 34779 bnj919 34781 bnj945 34787 bnj951 34789 bnj982 34792 bnj1019 34793 bnj518 34900 bnj571 34920 bnj594 34926 bnj916 34947 bnj966 34958 bnj967 34959 bnj1006 34974 bnj1018g 34977 bnj1018 34978 bnj1040 34986 bnj1174 35017 bnj1175 35018 bnj1311 35038 |
| Copyright terms: Public domain | W3C validator |