Metamath Proof Explorer

Theorem 3orit

Description: Closed form of 3ori . (Contributed by Scott Fenton, 20-Apr-2011)

Ref Expression
Assertion 3orit ⊢ φ ∨ ψ ∨ χ ↔ ¬ φ ∧ ¬ ψ → χ

Proof

Step Hyp Ref Expression
1 df-3or ⊢ φ ∨ ψ ∨ χ ↔ φ ∨ ψ ∨ χ
2 df-or ⊢ φ ∨ ψ ∨ χ ↔ ¬ φ ∨ ψ → χ
3 ioran ⊢ ¬ φ ∨ ψ ↔ ¬ φ ∧ ¬ ψ
4 3 imbi1i ⊢ ¬ φ ∨ ψ → χ ↔ ¬ φ ∧ ¬ ψ → χ
5 1 2 4 3bitri ⊢ φ ∨ ψ ∨ χ ↔ ¬ φ ∧ ¬ ψ → χ