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	|- ( ph -> -. th )
	3biorfd.2	|- ( ph -> -. ch )
Assertion	3bior2fd	|- ( ph -> ( ps <-> ( th \/ ch \/ ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		3biorfd.1	|- ( ph -> -. th )
2		3biorfd.2	|- ( ph -> -. ch )
3		biorf	|- ( -. ch -> ( ps <-> ( ch \/ ps ) ) )
4	2 3	syl	|- ( ph -> ( ps <-> ( ch \/ ps ) ) )
5	1	3bior1fd	|- ( ph -> ( ( ch \/ ps ) <-> ( th \/ ch \/ ps ) ) )
6	4 5	bitrd	|- ( ph -> ( ps <-> ( th \/ ch \/ ps ) ) )