![]() |
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 940 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒) |
4 | mpjao3dan.3 | . 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜒) | |
5 | mpjao3dan.4 | . . 3 ⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏)) | |
6 | df-3or 1069 | . . 3 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜏)) | |
7 | 5, 6 | sylib 210 | . 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ∨ 𝜏)) |
8 | 3, 4, 7 | mpjaodan 941 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∨ wo 833 ∨ w3o 1067 |
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 199 df-an 388 df-or 834 df-3or 1069 |
This theorem is referenced by: wemaplem2 8808 r1val1 9011 xleadd1a 12465 xlt2add 12472 xmullem 12476 xmulgt0 12495 xmulasslem3 12498 xlemul1a 12500 xadddilem 12506 xadddi 12507 xadddi2 12509 isxmet2d 22643 icccvx 23260 ivthicc 23765 mbfmulc2lem 23954 c1lip1 24300 dvivth 24313 reeff1o 24741 coseq00topi 24794 tanabsge 24798 logcnlem3 24931 atantan 25205 atanbnd 25208 cvxcl 25267 ostthlem1 25908 iscgrglt 26005 tgdim01ln 26055 lnxfr 26057 lnext 26058 tgfscgr 26059 tglineeltr 26122 colmid 26179 prodtp 30292 xrpxdivcld 30360 s3f1 30368 cyc3co2 30460 archirngz 30484 archiabllem1b 30487 esumcst 30966 sgnmulsgn 31453 sgnmulsgp 31454 hgt750lemb 31575 fnwe2lem3 39048 |
Copyright terms: Public domain | W3C validator |