This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 3biant1d

Description: A conjunction is equivalent to a threefold conjunction with single truth, analogous to biantrud . (Contributed by Alexander van der Vekens, 26-Sep-2017)

		Ref	Expression
	Hypothesis	3biantd.1	$⊢ φ \to θ$
	Assertion	3biant1d	$⊢ φ \to ((χ \land ψ) \leftrightarrow (θ \land χ \land ψ))$

Proof

Step	Hyp	Ref	Expression
1		3biantd.1	$⊢ φ \to θ$
2	1	biantrurd	$⊢ φ \to ((χ \land ψ) \leftrightarrow (θ \land (χ \land ψ)))$
3		3anass	$⊢ (θ \land χ \land ψ) \leftrightarrow (θ \land (χ \land ψ))$
4	2 3	bitr4di	$⊢ φ \to ((χ \land ψ) \leftrightarrow (θ \land χ \land ψ))$