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	⊢ ( 𝜑 → 𝜃 )
	Assertion	3biant1d	⊢ ( 𝜑 → ( ( 𝜒 ∧ 𝜓 ) ↔ ( 𝜃 ∧ 𝜒 ∧ 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		3biantd.1	⊢ ( 𝜑 → 𝜃 )
2	1	biantrurd	⊢ ( 𝜑 → ( ( 𝜒 ∧ 𝜓 ) ↔ ( 𝜃 ∧ ( 𝜒 ∧ 𝜓 ) ) ) )
3		3anass	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜓 ) ↔ ( 𝜃 ∧ ( 𝜒 ∧ 𝜓 ) ) )
4	2 3	bitr4di	⊢ ( 𝜑 → ( ( 𝜒 ∧ 𝜓 ) ↔ ( 𝜃 ∧ 𝜒 ∧ 𝜓 ) ) )