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 30005 | . 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) |
6 | 1, 2, 3 | w3a 1031 | . . 3 wff (𝜑 ∧ 𝜓 ∧ 𝜒) |
7 | 6, 4 | wa 383 | . 2 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) |
8 | 5, 7 | wb 195 | 1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) |
Colors of variables: wff setvar class |
This definition is referenced by: bnj248 30019 bnj250 30020 bnj258 30027 bnj268 30028 bnj291 30030 bnj312 30031 bnj446 30036 bnj645 30074 bnj658 30075 bnj887 30089 bnj919 30091 bnj945 30098 bnj951 30100 bnj982 30103 bnj1019 30104 bnj518 30210 bnj571 30230 bnj594 30236 bnj916 30257 bnj966 30268 bnj967 30269 bnj1006 30283 bnj1018 30286 bnj1040 30294 bnj1174 30325 bnj1175 30326 bnj1311 30346 |
Copyright terms: Public domain | W3C validator |