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 φ¬θ
3biorfd.2 φ¬χ
Assertion 3bior2fd φψθχψ

Proof

Step Hyp Ref Expression
1 3biorfd.1 φ¬θ
2 3biorfd.2 φ¬χ
3 biorf ¬χψχψ
4 2 3 syl φψχψ
5 1 3bior1fd φχψθχψ
6 4 5 bitrd φψθχψ