![]() |
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.) |
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 948 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒) |
4 | mpjao3dan.3 | . 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜒) | |
5 | mpjao3dan.4 | . . 3 ⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏)) | |
6 | df-3or 1072 | . . 3 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜏)) | |
7 | 5, 6 | sylib 208 | . 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ∨ 𝜏)) |
8 | 3, 4, 7 | mpjaodan 949 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 ∨ wo 826 ∨ w3o 1070 |
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 197 df-an 383 df-or 827 df-3or 1072 |
This theorem is referenced by: wemaplem2 8607 r1val1 8812 xleadd1a 12287 xlt2add 12294 xmullem 12298 xmulgt0 12317 xmulasslem3 12320 xlemul1a 12322 xadddilem 12328 xadddi 12329 xadddi2 12331 isxmet2d 22351 icccvx 22968 ivthicc 23445 mbfmulc2lem 23633 c1lip1 23979 dvivth 23992 reeff1o 24420 coseq00topi 24474 tanabsge 24478 logcnlem3 24610 atantan 24870 atanbnd 24873 cvxcl 24931 ostthlem1 25536 iscgrglt 25629 tgdim01ln 25679 lnxfr 25681 lnext 25682 tgfscgr 25683 tglineeltr 25746 colmid 25803 prodtp 29910 xrpxdivcld 29980 archirngz 30080 archiabllem1b 30083 esumcst 30462 sgnmulsgn 30948 sgnmulsgp 30949 hgt750lemb 31071 fnwe2lem3 38144 |
Copyright terms: Public domain | W3C validator |