|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > 3mix3d | Structured version Visualization version GIF version | ||
| Description: Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.) | 
| Ref | Expression | 
|---|---|
| 3mixd.1 | ⊢ (𝜑 → 𝜓) | 
| Ref | Expression | 
|---|---|
| 3mix3d | ⊢ (𝜑 → (𝜒 ∨ 𝜃 ∨ 𝜓)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | 3mixd.1 | . 2 ⊢ (𝜑 → 𝜓) | |
| 2 | 3mix3 1332 | . 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: xpord3inddlem 8180 elfiun 9471 nnnegz 12618 fvf1tp 13830 hashv01gt1 14385 lcmfunsnlem2lem2 16677 cshwshashlem1 17134 dyaddisjlem 25631 zabsle1 27341 noextendgt 27716 sltsolem1 27721 nodense 27738 btwncolg3 28566 btwnlng3 28630 frgr3vlem2 30294 3vfriswmgr 30298 frgrregorufr0 30344 weiunso 36468 fnwe2lem3 43069 omcl2 43351 gpgedgvtx1 48025 gpgvtxedg0 48026 gpgvtxedg1 48027 gpg3kgrtriexlem6 48049 eenglngeehlnmlem2 48664 | 
| Copyright terms: Public domain | W3C validator |