Metamath Proof Explorer


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 ( 𝜑 → ¬ 𝜃 )
Assertion 3bior1fd ( 𝜑 → ( ( 𝜒𝜓 ) ↔ ( 𝜃𝜒𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 3biorfd.1 ( 𝜑 → ¬ 𝜃 )
2 biorf ( ¬ 𝜃 → ( ( 𝜒𝜓 ) ↔ ( 𝜃 ∨ ( 𝜒𝜓 ) ) ) )
3 1 2 syl ( 𝜑 → ( ( 𝜒𝜓 ) ↔ ( 𝜃 ∨ ( 𝜒𝜓 ) ) ) )
4 3orass ( ( 𝜃𝜒𝜓 ) ↔ ( 𝜃 ∨ ( 𝜒𝜓 ) ) )
5 3 4 bitr4di ( 𝜑 → ( ( 𝜒𝜓 ) ↔ ( 𝜃𝜒𝜓 ) ) )