![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpjao3dan | GIF version |
Description: Eliminate a 3-way disjunction in a deduction. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
Ref | Expression |
---|---|
mpjao3dan.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
mpjao3dan.2 | ⊢ ((𝜑 ∧ 𝜃) → 𝜒) |
mpjao3dan.3 | ⊢ ((𝜑 ∧ 𝜏) → 𝜒) |
mpjao3dan.4 | ⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏)) |
Ref | Expression |
---|---|
mpjao3dan | ⊢ (𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpjao3dan.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
2 | mpjao3dan.2 | . . 3 ⊢ ((𝜑 ∧ 𝜃) → 𝜒) | |
3 | 1, 2 | jaodan 744 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒) |
4 | mpjao3dan.3 | . 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜒) | |
5 | mpjao3dan.4 | . . 3 ⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏)) | |
6 | df-3or 921 | . . 3 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜏)) | |
7 | 5, 6 | sylib 120 | . 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ∨ 𝜏)) |
8 | 3, 4, 7 | mpjaodan 745 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∨ wo 662 ∨ w3o 919 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 |
This theorem depends on definitions: df-bi 115 df-3or 921 |
This theorem is referenced by: wetriext 4327 nntri3 6141 nntri2or2 6142 caucvgprlemnkj 6918 caucvgprlemnbj 6919 caucvgprprlemnkj 6944 caucvgprprlemnbj 6945 caucvgsr 7040 addmodlteq 9480 sizefiv01gt1 9806 zdvdsdc 10361 divalglemeunn 10465 divalglemex 10466 divalglemeuneg 10467 divalg 10468 znege1 10700 |
Copyright terms: Public domain | W3C validator |