This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-bnj17

Description: Define the 4-way conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion df-bnj17 ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃 ) ↔ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 wph ⊢ 𝜑
1 wps ⊢ 𝜓
2 wch ⊢ 𝜒
3 wth ⊢ 𝜃
4 0 1 2 3 w-bnj17 ⊢ ( 𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃 )
5 0 1 2 w3a ⊢ ( 𝜑 ∧ 𝜓 ∧ 𝜒 )
6 5 3 wa ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ 𝜃 )
7 4 6 wb ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃 ) ↔ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) )