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 951 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒) |
4 | mpjao3dan.3 | . 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜒) | |
5 | mpjao3dan.4 | . . 3 ⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏)) | |
6 | df-3or 1080 | . . 3 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜏)) | |
7 | 5, 6 | sylib 219 | . 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ∨ 𝜏)) |
8 | 3, 4, 7 | mpjaodan 952 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∨ wo 841 ∨ w3o 1078 |
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 208 df-an 397 df-or 842 df-3or 1080 |
This theorem is referenced by: wemaplem2 8999 r1val1 9203 xleadd1a 12634 xlt2add 12641 xmullem 12645 xmulgt0 12664 xmulasslem3 12667 xlemul1a 12669 xadddilem 12675 xadddi 12676 xadddi2 12678 isxmet2d 22864 icccvx 23481 ivthicc 23986 mbfmulc2lem 24175 c1lip1 24521 dvivth 24534 reeff1o 24962 coseq00topi 25015 tanabsge 25019 logcnlem3 25154 atantan 25428 atanbnd 25431 cvxcl 25489 ostthlem1 26130 iscgrglt 26227 tgdim01ln 26277 lnxfr 26279 lnext 26280 tgfscgr 26281 tglineeltr 26344 colmid 26401 prodtp 30470 xrpxdivcld 30538 s3f1 30550 cycpmco2 30702 cyc3co2 30709 archirngz 30745 archiabllem1b 30748 esumcst 31221 sgnmulsgn 31706 sgnmulsgp 31707 hgt750lemb 31826 fnwe2lem3 39530 |
Copyright terms: Public domain | W3C validator |