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 1330 | . 2 ⊢ (𝜓 → (𝜒 ∨ 𝜓 ∨ 𝜃)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝜒 ∨ 𝜓 ∨ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ w3o 1085 |
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 1087 |
This theorem is referenced by: sosn 5674 f1dom3fv3dif 7138 f1dom3el3dif 7139 elfiun 9177 fpwwe2lem12 10409 swrdnd0 14381 lcmfunsnlem2lem2 16355 dyaddisjlem 24770 tgcolg 26926 btwncolg2 26928 hlln 26979 btwnlng2 26992 frgrregorufr0 28697 xpord3ind 33809 sltsolem1 33887 colineartriv2 34379 eenglngeehlnmlem2 46063 |
Copyright terms: Public domain | W3C validator |