Metamath Proof Explorer
Description: Deduction for elimination by cases. (Contributed by NM, 21-Apr-1994)
(Proof shortened by Wolf Lammen, 22-Dec-2012)
|
|
Ref |
Expression |
|
Hypotheses |
ecase2d.1 |
⊢ ( 𝜑 → 𝜓 ) |
|
|
ecase2d.2 |
⊢ ( 𝜑 → ¬ ( 𝜓 ∧ 𝜒 ) ) |
|
|
ecase2d.3 |
⊢ ( 𝜑 → ¬ ( 𝜓 ∧ 𝜃 ) ) |
|
|
ecase2d.4 |
⊢ ( 𝜑 → ( 𝜏 ∨ ( 𝜒 ∨ 𝜃 ) ) ) |
|
Assertion |
ecase2d |
⊢ ( 𝜑 → 𝜏 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
ecase2d.1 |
⊢ ( 𝜑 → 𝜓 ) |
2 |
|
ecase2d.2 |
⊢ ( 𝜑 → ¬ ( 𝜓 ∧ 𝜒 ) ) |
3 |
|
ecase2d.3 |
⊢ ( 𝜑 → ¬ ( 𝜓 ∧ 𝜃 ) ) |
4 |
|
ecase2d.4 |
⊢ ( 𝜑 → ( 𝜏 ∨ ( 𝜒 ∨ 𝜃 ) ) ) |
5 |
|
idd |
⊢ ( 𝜑 → ( 𝜏 → 𝜏 ) ) |
6 |
2
|
pm2.21d |
⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜒 ) → 𝜏 ) ) |
7 |
1 6
|
mpand |
⊢ ( 𝜑 → ( 𝜒 → 𝜏 ) ) |
8 |
3
|
pm2.21d |
⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜃 ) → 𝜏 ) ) |
9 |
1 8
|
mpand |
⊢ ( 𝜑 → ( 𝜃 → 𝜏 ) ) |
10 |
7 9
|
jaod |
⊢ ( 𝜑 → ( ( 𝜒 ∨ 𝜃 ) → 𝜏 ) ) |
11 |
5 10 4
|
mpjaod |
⊢ ( 𝜑 → 𝜏 ) |