Theorem bnj252 35037

Description: ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)

Assertion

Ref	Expression
bnj252	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)))

Proof of Theorem bnj252

Step	Hyp	Ref	Expression
1		bnj250 35035	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)))
2		df-3an 1103	. . 3 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜃))
3	2	anbi2i 634	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)))
4	1, 3	bitr4i 281	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   ∧ w-bnj17 35020

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-bnj17 35021

This theorem is referenced by:  bnj290  35044  bnj563  35077  bnj919  35101  bnj976  35111  bnj543  35226  bnj570  35238  bnj594  35245  bnj916  35266  bnj917  35267  bnj964  35276  bnj983  35284  bnj984  35285  bnj998  35290  bnj999  35291  bnj1021  35299  bnj1083  35311  bnj1450  35383