Description: Distributive law for disjunction. Theorem *4.41 of WhiteheadRussell p. 119. (Contributed by NM, 5-Jan-1993) (Proof shortened by Andrew Salmon, 7-May-2011) (Proof shortened by Wolf Lammen, 28-Nov-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ordi | ⊢ ( ( 𝜑 ∨ ( 𝜓 ∧ 𝜒 ) ) ↔ ( ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | jcab | ⊢ ( ( ¬ 𝜑 → ( 𝜓 ∧ 𝜒 ) ) ↔ ( ( ¬ 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) ) | |
| 2 | df-or | ⊢ ( ( 𝜑 ∨ ( 𝜓 ∧ 𝜒 ) ) ↔ ( ¬ 𝜑 → ( 𝜓 ∧ 𝜒 ) ) ) | |
| 3 | df-or | ⊢ ( ( 𝜑 ∨ 𝜓 ) ↔ ( ¬ 𝜑 → 𝜓 ) ) | |
| 4 | df-or | ⊢ ( ( 𝜑 ∨ 𝜒 ) ↔ ( ¬ 𝜑 → 𝜒 ) ) | |
| 5 | 3 4 | anbi12i | ⊢ ( ( ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) ↔ ( ( ¬ 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) ) |
| 6 | 1 2 5 | 3bitr4i | ⊢ ( ( 𝜑 ∨ ( 𝜓 ∧ 𝜒 ) ) ↔ ( ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) ) |