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