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 ⊢ φ ∨ ψ ↔ χ ↔ φ ∨ ψ ↔ φ ∨ χ