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

Metamath Proof Explorer

Theorem 3bior2fd

Description: A wff is equivalent to its threefold disjunction with double falsehood, analogous to biorf . (Contributed by Alexander van der Vekens, 8-Sep-2017)

	Ref	Expression
Hypotheses	3biorfd.1	$⊢ φ \to \neg θ$
	3biorfd.2	$⊢ φ \to \neg χ$
Assertion	3bior2fd	$⊢ φ \to (ψ \leftrightarrow (θ \lor χ \lor ψ))$

Proof

Step	Hyp	Ref	Expression
1		3biorfd.1	$⊢ φ \to \neg θ$
2		3biorfd.2	$⊢ φ \to \neg χ$
3		biorf	$⊢ \neg χ \to (ψ \leftrightarrow (χ \lor ψ))$
4	2 3	syl	$⊢ φ \to (ψ \leftrightarrow (χ \lor ψ))$
5	1	3bior1fd	$⊢ φ \to ((χ \lor ψ) \leftrightarrow (θ \lor χ \lor ψ))$
6	4 5	bitrd	$⊢ φ \to (ψ \leftrightarrow (θ \lor χ \lor ψ))$