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 1323 | . 2 ⊢ (𝜓 → (𝜒 ∨ 𝜓 ∨ 𝜃)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝜒 ∨ 𝜓 ∨ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ w3o 1078 |
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 208 df-or 842 df-3or 1080 |
This theorem is referenced by: sosn 5631 f1dom3fv3dif 7017 f1dom3el3dif 7018 elfiun 8882 fpwwe2lem13 10052 swrdnd0 14007 lcmfunsnlem2lem2 15971 dyaddisjlem 24123 tgcolg 26267 btwncolg2 26269 hlln 26320 btwnlng2 26333 frgrregorufr0 28030 sltsolem1 33077 colineartriv2 33426 eenglngeehlnmlem2 44653 |
Copyright terms: Public domain | W3C validator |