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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3biorfd.1 | |
|
2 | 3biorfd.2 | |
|
3 | biorf | |
|
4 | 2 3 | syl | |
5 | 1 | 3bior1fd | |
6 | 4 5 | bitrd | |