![]() |
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 31633 | . 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) |
6 | 1, 2, 3 | w3a 1068 | . . 3 wff (𝜑 ∧ 𝜓 ∧ 𝜒) |
7 | 6, 4 | wa 387 | . 2 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) |
8 | 5, 7 | wb 198 | 1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) |
Colors of variables: wff setvar class |
This definition is referenced by: bnj248 31647 bnj250 31648 bnj258 31655 bnj268 31656 bnj291 31658 bnj312 31659 bnj446 31664 bnj645 31698 bnj658 31699 bnj887 31713 bnj919 31715 bnj945 31722 bnj951 31724 bnj982 31727 bnj1019 31728 bnj518 31834 bnj571 31854 bnj594 31860 bnj916 31881 bnj966 31892 bnj967 31893 bnj1006 31907 bnj1018 31910 bnj1040 31918 bnj1174 31949 bnj1175 31950 bnj1311 31970 |
Copyright terms: Public domain | W3C validator |