![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpjao3dan | Structured version Visualization version GIF version |
Description: Eliminate a three-way disjunction in a deduction. (Contributed by Thierry Arnoux, 13-Apr-2018.) (Proof shortened by Wolf Lammen, 20-Apr-2024.) |
Ref | Expression |
---|---|
mpjao3dan.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
mpjao3dan.2 | ⊢ ((𝜑 ∧ 𝜃) → 𝜒) |
mpjao3dan.3 | ⊢ ((𝜑 ∧ 𝜏) → 𝜒) |
mpjao3dan.4 | ⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏)) |
Ref | Expression |
---|---|
mpjao3dan | ⊢ (𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpjao3dan.4 | . 2 ⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏)) | |
2 | mpjao3dan.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
3 | mpjao3dan.2 | . . 3 ⊢ ((𝜑 ∧ 𝜃) → 𝜒) | |
4 | mpjao3dan.3 | . . 3 ⊢ ((𝜑 ∧ 𝜏) → 𝜒) | |
5 | 2, 3, 4 | 3jaodan 1427 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒) |
6 | 1, 5 | mpdan 685 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∨ w3o 1083 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 |
This theorem is referenced by: wemaplem2 9572 r1val1 9811 xleadd1a 13267 xlt2add 13274 xmullem 13278 xmulgt0 13297 xmulasslem3 13300 xlemul1a 13302 xadddilem 13308 xadddi 13309 xadddi2 13311 isxmet2d 24277 icccvx 24919 ivthicc 25431 mbfmulc2lem 25620 c1lip1 25974 dvivth 25987 reeff1o 26429 coseq00topi 26482 tanabsge 26486 logcnlem3 26623 atantan 26900 atanbnd 26903 cvxcl 26962 ostthlem1 27605 iscgrglt 28390 tgdim01ln 28440 lnxfr 28442 lnext 28443 tgfscgr 28444 tglineeltr 28507 colmid 28564 prodtp 32675 xrpxdivcld 32743 s3f1 32757 cycpmco2 32946 cyc3co2 32953 archirngz 32989 archiabllem1b 32992 esumcst 33810 sgnmulsgn 34297 sgnmulsgp 34298 hgt750lemb 34416 exp11d 42017 fnwe2lem3 42615 |
Copyright terms: Public domain | W3C validator |