Description: Closed form of 3ori . (Contributed by Scott Fenton, 20-Apr-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | 3orit | ⊢ ( ( 𝜑 ∨ 𝜓 ∨ 𝜒 ) ↔ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) → 𝜒 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3or | ⊢ ( ( 𝜑 ∨ 𝜓 ∨ 𝜒 ) ↔ ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) ) | |
2 | df-or | ⊢ ( ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) ↔ ( ¬ ( 𝜑 ∨ 𝜓 ) → 𝜒 ) ) | |
3 | ioran | ⊢ ( ¬ ( 𝜑 ∨ 𝜓 ) ↔ ( ¬ 𝜑 ∧ ¬ 𝜓 ) ) | |
4 | 3 | imbi1i | ⊢ ( ( ¬ ( 𝜑 ∨ 𝜓 ) → 𝜒 ) ↔ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) → 𝜒 ) ) |
5 | 1 2 4 | 3bitri | ⊢ ( ( 𝜑 ∨ 𝜓 ∨ 𝜒 ) ↔ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) → 𝜒 ) ) |