![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3mix2d | Structured version Visualization version GIF version |
Description: Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.) |
Ref | Expression |
---|---|
3mixd.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
3mix2d | ⊢ (𝜑 → (𝜒 ∨ 𝜓 ∨ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3mixd.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | 3mix2 1328 | . 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: sosn 5766 f1dom3fv3dif 7282 f1dom3el3dif 7283 xpord3inddlem 8163 elfiun 9459 fpwwe2lem12 10671 swrdnd0 14645 lcmfunsnlem2lem2 16615 dyaddisjlem 25542 sltsolem1 27626 tgcolg 28376 btwncolg2 28378 hlln 28429 btwnlng2 28442 frgrregorufr0 30152 colineartriv2 35669 eenglngeehlnmlem2 47862 |
Copyright terms: Public domain | W3C validator |