![]() |
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 845 df-3or 1085 |
This theorem is referenced by: sosn 5755 f1dom3fv3dif 7262 f1dom3el3dif 7263 xpord3inddlem 8137 elfiun 9424 fpwwe2lem12 10636 swrdnd0 14611 lcmfunsnlem2lem2 16581 dyaddisjlem 25475 sltsolem1 27559 tgcolg 28309 btwncolg2 28311 hlln 28362 btwnlng2 28375 frgrregorufr0 30082 colineartriv2 35573 eenglngeehlnmlem2 47680 |
Copyright terms: Public domain | W3C validator |