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