Metamath Proof Explorer


Theorem 3bior1fand

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

Ref Expression
Hypothesis 3biorfd.1 φ¬θ
Assertion 3bior1fand φχψθτχψ

Proof

Step Hyp Ref Expression
1 3biorfd.1 φ¬θ
2 1 intnanrd φ¬θτ
3 2 3bior1fd φχψθτχψ