Description: In a conjunctive normal form a pair of nodes like ( ph \/ ps ) /\ ( -. ph \/ ch ) eliminates the need of a node ( ps \/ ch ) . This theorem allows simplifications in that respect. (Contributed by Wolf Lammen, 20-Jun-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wl-orel12 | ⊢ ( ( ( 𝜑 ∨ 𝜓 ) ∧ ( ¬ 𝜑 ∨ 𝜒 ) ) → ( 𝜓 ∨ 𝜒 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm2.1 | ⊢ ( ¬ 𝜑 ∨ 𝜑 ) | |
| 2 | orel1 | ⊢ ( ¬ 𝜑 → ( ( 𝜑 ∨ 𝜓 ) → 𝜓 ) ) | |
| 3 | orc | ⊢ ( 𝜓 → ( 𝜓 ∨ 𝜒 ) ) | |
| 4 | 2 3 | syl6com | ⊢ ( ( 𝜑 ∨ 𝜓 ) → ( ¬ 𝜑 → ( 𝜓 ∨ 𝜒 ) ) ) |
| 5 | notnot | ⊢ ( 𝜑 → ¬ ¬ 𝜑 ) | |
| 6 | orel1 | ⊢ ( ¬ ¬ 𝜑 → ( ( ¬ 𝜑 ∨ 𝜒 ) → 𝜒 ) ) | |
| 7 | 5 6 | syl | ⊢ ( 𝜑 → ( ( ¬ 𝜑 ∨ 𝜒 ) → 𝜒 ) ) |
| 8 | olc | ⊢ ( 𝜒 → ( 𝜓 ∨ 𝜒 ) ) | |
| 9 | 7 8 | syl6com | ⊢ ( ( ¬ 𝜑 ∨ 𝜒 ) → ( 𝜑 → ( 𝜓 ∨ 𝜒 ) ) ) |
| 10 | 4 9 | jaao | ⊢ ( ( ( 𝜑 ∨ 𝜓 ) ∧ ( ¬ 𝜑 ∨ 𝜒 ) ) → ( ( ¬ 𝜑 ∨ 𝜑 ) → ( 𝜓 ∨ 𝜒 ) ) ) |
| 11 | 1 10 | mpi | ⊢ ( ( ( 𝜑 ∨ 𝜓 ) ∧ ( ¬ 𝜑 ∨ 𝜒 ) ) → ( 𝜓 ∨ 𝜒 ) ) |