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

Metamath Proof Explorer

Theorem triantru3

Description: A wff is equivalent to its conjunctions with truths. (Contributed by Peter Mazsa, 30-Nov-2018)

	Ref	Expression
Hypotheses	triantru3.1	$⊢ φ$
	triantru3.2	$⊢ ψ$
Assertion	triantru3	$⊢ χ \leftrightarrow (φ \land ψ \land χ)$

Step	Hyp	Ref	Expression
1		triantru3.1	$⊢ φ$
2		triantru3.2	$⊢ ψ$
3	1	biantrur	$⊢ (ψ \land χ) \leftrightarrow (φ \land (ψ \land χ))$
4	2	biantrur	$⊢ χ \leftrightarrow (ψ \land χ)$
5		3anass	$⊢ (φ \land ψ \land χ) \leftrightarrow (φ \land (ψ \land χ))$
6	3 4 5	3bitr4i	$⊢ χ \leftrightarrow (φ \land ψ \land χ)$