Theorem bnj252 32083

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 32081	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)))
2		df-3an 1086	. . 3 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜃))
3	2	anbi2i 625	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)))
4	1, 3	bitr4i 281	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)))

Syntax hints:   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   ∧ w-bnj17 32066

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 400  df-3an 1086  df-bnj17 32067

This theorem is referenced by:  bnj290  32090  bnj563  32124  bnj919  32148  bnj976  32159  bnj543  32275  bnj570  32287  bnj594  32294  bnj916  32315  bnj917  32316  bnj964  32325  bnj983  32333  bnj984  32334  bnj998  32339  bnj999  32340  bnj1021  32348  bnj1083  32360  bnj1450  32432