Metamath Proof Explorer


Theorem orbidi

Description: Disjunction distributes over the biconditional. An axiom of system DS in Vladimir Lifschitz, "On calculational proofs" (1998), http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.3384 . (Contributed by NM, 8-Jan-2005) (Proof shortened by Wolf Lammen, 4-Feb-2013)

Ref Expression
Assertion orbidi ( ( 𝜑 ∨ ( 𝜓𝜒 ) ) ↔ ( ( 𝜑𝜓 ) ↔ ( 𝜑𝜒 ) ) )

Proof

Step Hyp Ref Expression
1 pm5.74 ( ( ¬ 𝜑 → ( 𝜓𝜒 ) ) ↔ ( ( ¬ 𝜑𝜓 ) ↔ ( ¬ 𝜑𝜒 ) ) )
2 df-or ( ( 𝜑 ∨ ( 𝜓𝜒 ) ) ↔ ( ¬ 𝜑 → ( 𝜓𝜒 ) ) )
3 df-or ( ( 𝜑𝜓 ) ↔ ( ¬ 𝜑𝜓 ) )
4 df-or ( ( 𝜑𝜒 ) ↔ ( ¬ 𝜑𝜒 ) )
5 3 4 bibi12i ( ( ( 𝜑𝜓 ) ↔ ( 𝜑𝜒 ) ) ↔ ( ( ¬ 𝜑𝜓 ) ↔ ( ¬ 𝜑𝜒 ) ) )
6 1 2 5 3bitr4i ( ( 𝜑 ∨ ( 𝜓𝜒 ) ) ↔ ( ( 𝜑𝜓 ) ↔ ( 𝜑𝜒 ) ) )