Theorem bnj252 33745

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 33743	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)))
2		df-3an 1090	. . 3 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜃))
3	2	anbi2i 624	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)))
4	1, 3	bitr4i 278	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)))

Syntax hints:   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   ∧ w-bnj17 33728

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 206  df-an 398  df-3an 1090  df-bnj17 33729

This theorem is referenced by:  bnj290  33752  bnj563  33785  bnj919  33809  bnj976  33819  bnj543  33935  bnj570  33947  bnj594  33954  bnj916  33975  bnj917  33976  bnj964  33985  bnj983  33993  bnj984  33994  bnj998  33999  bnj999  34000  bnj1021  34008  bnj1083  34020  bnj1450  34092