![]() |
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 34188 | . 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) |
6 | 1, 2, 3 | w3a 1084 | . . 3 wff (𝜑 ∧ 𝜓 ∧ 𝜒) |
7 | 6, 4 | wa 395 | . 2 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) |
8 | 5, 7 | wb 205 | 1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) |
Colors of variables: wff setvar class |
This definition is referenced by: bnj248 34202 bnj250 34203 bnj258 34210 bnj268 34211 bnj291 34213 bnj312 34214 bnj446 34219 bnj645 34252 bnj658 34253 bnj887 34267 bnj919 34269 bnj945 34275 bnj951 34277 bnj982 34280 bnj1019 34281 bnj518 34388 bnj571 34408 bnj594 34414 bnj916 34435 bnj966 34446 bnj967 34447 bnj1006 34462 bnj1018g 34465 bnj1018 34466 bnj1040 34474 bnj1174 34505 bnj1175 34506 bnj1311 34526 |
Copyright terms: Public domain | W3C validator |