![]() |
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 1431 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒) |
6 | 1, 5 | mpdan 686 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∨ w3o 1087 |
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 398 df-or 847 df-3or 1089 df-3an 1090 |
This theorem is referenced by: wemaplem2 9491 r1val1 9730 xleadd1a 13181 xlt2add 13188 xmullem 13192 xmulgt0 13211 xmulasslem3 13214 xlemul1a 13216 xadddilem 13222 xadddi 13223 xadddi2 13225 isxmet2d 23703 icccvx 24336 ivthicc 24845 mbfmulc2lem 25034 c1lip1 25384 dvivth 25397 reeff1o 25829 coseq00topi 25882 tanabsge 25886 logcnlem3 26022 atantan 26296 atanbnd 26299 cvxcl 26357 ostthlem1 26998 iscgrglt 27505 tgdim01ln 27555 lnxfr 27557 lnext 27558 tgfscgr 27559 tglineeltr 27622 colmid 27679 prodtp 31779 xrpxdivcld 31847 s3f1 31859 cycpmco2 32038 cyc3co2 32045 archirngz 32081 archiabllem1b 32084 esumcst 32726 sgnmulsgn 33213 sgnmulsgp 33214 hgt750lemb 33333 exp11d 40858 fnwe2lem3 41426 |
Copyright terms: Public domain | W3C validator |