Description: Distributive law for conjunction. Theorem *4.4 of WhiteheadRussell p. 118. (Contributed by NM, 21-Jun-1993) (Proof shortened by Wolf Lammen, 5-Jan-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | andi | ⊢ ( ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ∧ 𝜒 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | orc | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ∧ 𝜒 ) ) ) | |
| 2 | olc | ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ∧ 𝜒 ) ) ) | |
| 3 | 1 2 | jaodan | ⊢ ( ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) → ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ∧ 𝜒 ) ) ) |
| 4 | orc | ⊢ ( 𝜓 → ( 𝜓 ∨ 𝜒 ) ) | |
| 5 | 4 | anim2i | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) ) |
| 6 | olc | ⊢ ( 𝜒 → ( 𝜓 ∨ 𝜒 ) ) | |
| 7 | 6 | anim2i | ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) ) |
| 8 | 5 7 | jaoi | ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ∧ 𝜒 ) ) → ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) ) |
| 9 | 3 8 | impbii | ⊢ ( ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ∧ 𝜒 ) ) ) |