|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > 3mix1d | Structured version Visualization version GIF version | ||
| Description: Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.) | 
| Ref | Expression | 
|---|---|
| 3mixd.1 | ⊢ (𝜑 → 𝜓) | 
| Ref | Expression | 
|---|---|
| 3mix1d | ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜃)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | 3mixd.1 | . 2 ⊢ (𝜑 → 𝜓) | |
| 2 | 3mix1 1330 | . 2 ⊢ (𝜓 → (𝜓 ∨ 𝜒 ∨ 𝜃)) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜃)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∨ 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-or 848 df-3or 1087 | 
| This theorem is referenced by: f1dom3fv3dif 7289 f1dom3el3dif 7290 xpord3inddlem 8180 elfiun 9471 prinfzo0 13739 fvf1tp 13830 lcmfunsnlem2lem2 16677 estrreslem2 18184 ostth 27684 noextendlt 27715 sltsolem1 27721 nodense 27738 btwncolg1 28564 hlln 28616 btwnlng1 28628 colineartriv1 36069 weiunso 36468 fnwe2lem3 43069 dfxlim2v 45867 gpgedgvtx0 48024 gpgvtxedg0 48026 gpgvtxedg1 48027 eenglngeehlnmlem2 48664 | 
| Copyright terms: Public domain | W3C validator |