Theorem 3bior1fd

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

	Ref	Expression
Hypothesis	3biorfd.1	|- ( ph -> -. th )
Assertion	3bior1fd	|- ( ph -> ( ( ch \/ ps ) <-> ( th \/ ch \/ ps ) ) )

Proof

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