Theorem bnj252 34886

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   ∧ w-bnj17 34869

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 207  df-an 396  df-3an 1089  df-bnj17 34870

This theorem is referenced by:  bnj290  34893  bnj563  34926  bnj919  34950  bnj976  34960  bnj543  35075  bnj570  35087  bnj594  35094  bnj916  35115  bnj917  35116  bnj964  35125  bnj983  35133  bnj984  35134  bnj998  35139  bnj999  35140  bnj1021  35148  bnj1083  35160  bnj1450  35232