![]() |
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 1430 | . 2 ⊢ (𝜓 → (𝜓 ∨ 𝜒 ∨ 𝜃)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ w3o 1107 |
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-or 875 df-3or 1109 |
This theorem is referenced by: f1dom3fv3dif 6753 f1dom3el3dif 6754 elfiun 8578 prinfzo0 12762 lcmfunsnlem2lem2 15687 estrreslem2 17092 ostth 25680 btwncolg1 25806 hlln 25858 btwnlng1 25870 noextendlt 32335 sltsolem1 32339 nodense 32355 colineartriv1 32687 fnwe2lem3 38407 dfxlim2v 40817 |
Copyright terms: Public domain | W3C validator |