Theorem bnj887

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

	Ref	Expression
Hypotheses	bnj887.1	⊢ ( 𝜑 ↔ 𝜑′ )
	bnj887.2	⊢ ( 𝜓 ↔ 𝜓′ )
	bnj887.3	⊢ ( 𝜒 ↔ 𝜒′ )
	bnj887.4	⊢ ( 𝜃 ↔ 𝜃′ )
Assertion	bnj887	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃 ) ↔ ( 𝜑′ ∧ 𝜓′ ∧ 𝜒′ ∧ 𝜃′ ) )

Proof

Step	Hyp	Ref	Expression
1		bnj887.1	⊢ ( 𝜑 ↔ 𝜑′ )
2		bnj887.2	⊢ ( 𝜓 ↔ 𝜓′ )
3		bnj887.3	⊢ ( 𝜒 ↔ 𝜒′ )
4		bnj887.4	⊢ ( 𝜃 ↔ 𝜃′ )
5	1 2 3	3anbi123i	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( 𝜑′ ∧ 𝜓′ ∧ 𝜒′ ) )
6	5 4	anbi12i	⊢ ( ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) ↔ ( ( 𝜑′ ∧ 𝜓′ ∧ 𝜒′ ) ∧ 𝜃′ ) )
7		df-bnj17	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃 ) ↔ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) )
8		df-bnj17	⊢ ( ( 𝜑′ ∧ 𝜓′ ∧ 𝜒′ ∧ 𝜃′ ) ↔ ( ( 𝜑′ ∧ 𝜓′ ∧ 𝜒′ ) ∧ 𝜃′ ) )
9	6 7 8	3bitr4i	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃 ) ↔ ( 𝜑′ ∧ 𝜓′ ∧ 𝜒′ ∧ 𝜃′ ) )