Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3mix3d | Structured version Visualization version GIF version |
Description: Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.) |
Ref | Expression |
---|---|
3mixd.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
3mix3d | ⊢ (𝜑 → (𝜒 ∨ 𝜃 ∨ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3mixd.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | 3mix3 1334 | . 2 ⊢ (𝜓 → (𝜒 ∨ 𝜃 ∨ 𝜓)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝜒 ∨ 𝜃 ∨ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ w3o 1088 |
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 210 df-or 848 df-3or 1090 |
This theorem is referenced by: elfiun 9071 nnnegz 12204 hashv01gt1 13936 lcmfunsnlem2lem2 16221 cshwshashlem1 16674 dyaddisjlem 24516 zabsle1 26201 btwncolg3 26672 btwnlng3 26736 frgr3vlem2 28381 3vfriswmgr 28385 frgrregorufr0 28431 xpord3ind 33563 noextendgt 33636 sltsolem1 33641 nodense 33658 fnwe2lem3 40609 eenglngeehlnmlem2 45786 |
Copyright terms: Public domain | W3C validator |