| 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 1332 | . 2 ⊢ (𝜓 → (𝜒 ∨ 𝜓 ∨ 𝜃)) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝜒 ∨ 𝜓 ∨ 𝜃)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∨ w3o 1086 |
| 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 207 df-or 849 df-3or 1088 |
| This theorem is referenced by: sosn 5772 f1dom3fv3dif 7288 f1dom3el3dif 7289 xpord3inddlem 8179 elfiun 9470 fpwwe2lem12 10682 fvf1tp 13829 swrdnd0 14695 lcmfunsnlem2lem2 16676 dyaddisjlem 25630 sltsolem1 27720 tgcolg 28562 btwncolg2 28564 hlln 28615 btwnlng2 28628 frgrregorufr0 30343 constrsslem 33782 colineartriv2 36069 gpgvtxedg0 48021 gpgvtxedg1 48022 eenglngeehlnmlem2 48659 |
| Copyright terms: Public domain | W3C validator |