Theorem bnj252 34901

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 34899	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)))
2		df-3an 1095	. . 3 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜃))
3	2	anbi2i 630	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)))
4	1, 3	bitr4i 280	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)))

Syntax hints:   ↔ wb 208   ∧ wa 397   ∧ w3a 1093   ∧ w-bnj17 34884

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 209  df-an 398  df-3an 1095  df-bnj17 34885

This theorem is referenced by:  bnj290  34908  bnj563  34941  bnj919  34965  bnj976  34975  bnj543  35090  bnj570  35102  bnj594  35109  bnj916  35130  bnj917  35131  bnj964  35140  bnj983  35148  bnj984  35149  bnj998  35154  bnj999  35155  bnj1021  35163  bnj1083  35175  bnj1450  35247