Description: Implication distributes over disjunction. Theorem *4.78 of WhiteheadRussell p. 121. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 19-Nov-2012)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | pm4.78 | ⊢ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜑 → 𝜒 ) ) ↔ ( 𝜑 → ( 𝜓 ∨ 𝜒 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | orordi | ⊢ ( ( ¬ 𝜑 ∨ ( 𝜓 ∨ 𝜒 ) ) ↔ ( ( ¬ 𝜑 ∨ 𝜓 ) ∨ ( ¬ 𝜑 ∨ 𝜒 ) ) ) | |
| 2 | imor | ⊢ ( ( 𝜑 → ( 𝜓 ∨ 𝜒 ) ) ↔ ( ¬ 𝜑 ∨ ( 𝜓 ∨ 𝜒 ) ) ) | |
| 3 | imor | ⊢ ( ( 𝜑 → 𝜓 ) ↔ ( ¬ 𝜑 ∨ 𝜓 ) ) | |
| 4 | imor | ⊢ ( ( 𝜑 → 𝜒 ) ↔ ( ¬ 𝜑 ∨ 𝜒 ) ) | |
| 5 | 3 4 | orbi12i | ⊢ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜑 → 𝜒 ) ) ↔ ( ( ¬ 𝜑 ∨ 𝜓 ) ∨ ( ¬ 𝜑 ∨ 𝜒 ) ) ) |
| 6 | 1 2 5 | 3bitr4ri | ⊢ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜑 → 𝜒 ) ) ↔ ( 𝜑 → ( 𝜓 ∨ 𝜒 ) ) ) |