![]() |
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 1327 | . 2 ⊢ (𝜓 → (𝜓 ∨ 𝜒 ∨ 𝜃)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ w3o 1083 |
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-or 846 df-3or 1085 |
This theorem is referenced by: f1dom3fv3dif 7273 f1dom3el3dif 7274 xpord3inddlem 8158 elfiun 9464 prinfzo0 13717 lcmfunsnlem2lem2 16633 estrreslem2 18155 ostth 27663 noextendlt 27694 sltsolem1 27700 nodense 27717 btwncolg1 28477 hlln 28529 btwnlng1 28541 colineartriv1 35902 fnwe2lem3 42748 dfxlim2v 45502 eenglngeehlnmlem2 48160 |
Copyright terms: Public domain | W3C validator |