|   | 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 1432 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒) | 
| 6 | 1, 5 | mpdan 687 | 1 ⊢ (𝜑 → 𝜒) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∨ w3o 1085 | 
| 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 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 | 
| This theorem is referenced by: wemaplem2 9588 r1val1 9827 xleadd1a 13296 xlt2add 13303 xmullem 13307 xmulgt0 13326 xmulasslem3 13329 xlemul1a 13331 xadddilem 13337 xadddi 13338 xadddi2 13340 isxmet2d 24338 icccvx 24982 ivthicc 25494 mbfmulc2lem 25683 c1lip1 26037 dvivth 26050 reeff1o 26492 coseq00topi 26545 tanabsge 26549 logcnlem3 26687 atantan 26967 atanbnd 26970 cvxcl 27029 ostthlem1 27672 iscgrglt 28523 tgdim01ln 28573 lnxfr 28575 lnext 28576 tgfscgr 28577 tglineeltr 28640 colmid 28697 prodtp 32830 xrpxdivcld 32918 s3f1 32932 gsumtp 33062 cycpmco2 33154 cyc3co2 33161 archirngz 33197 archiabllem1b 33200 constrelextdg2 33789 esumcst 34065 sgnmulsgn 34553 sgnmulsgp 34554 hgt750lemb 34672 weiunso 36468 exp11d 42366 fnwe2lem3 43069 | 
| Copyright terms: Public domain | W3C validator |