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 30752 | . 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) |
6 | 1, 2, 3 | w3a 1037 | . . 3 wff (𝜑 ∧ 𝜓 ∧ 𝜒) |
7 | 6, 4 | wa 384 | . 2 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) |
8 | 5, 7 | wb 196 | 1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) |
Colors of variables: wff setvar class |
This definition is referenced by: bnj248 30766 bnj250 30767 bnj258 30774 bnj268 30775 bnj291 30777 bnj312 30778 bnj446 30783 bnj645 30820 bnj658 30821 bnj887 30835 bnj919 30837 bnj945 30844 bnj951 30846 bnj982 30849 bnj1019 30850 bnj518 30956 bnj571 30976 bnj594 30982 bnj916 31003 bnj966 31014 bnj967 31015 bnj1006 31029 bnj1018 31032 bnj1040 31040 bnj1174 31071 bnj1175 31072 bnj1311 31092 |
Copyright terms: Public domain | W3C validator |