![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3mix2 | Structured version Visualization version GIF version |
Description: Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.) |
Ref | Expression |
---|---|
3mix2 | ⊢ (𝜑 → (𝜓 ∨ 𝜑 ∨ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3mix1 1330 | . 2 ⊢ (𝜑 → (𝜑 ∨ 𝜒 ∨ 𝜓)) | |
2 | 3orrot 1091 | . 2 ⊢ ((𝜓 ∨ 𝜑 ∨ 𝜒) ↔ (𝜑 ∨ 𝜒 ∨ 𝜓)) | |
3 | 1, 2 | sylibr 234 | 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 207 df-or 848 df-3or 1087 |
This theorem is referenced by: 3mix2i 1334 3mix2d 1337 3jaobOLD 1427 tppreqb 4811 tpres 7225 onzsl 7871 sornom 10321 nnz 12638 nn0le2is012 12686 hash1to3 14534 cshwshashlem1 17136 zabsle1 27363 ostth 27706 nolesgn2o 27739 nogesgn1o 27741 sltsolem1 27743 nosep1o 27749 nosep2o 27750 nodenselem8 27759 fnwe2lem3 43055 dfxlim2v 45814 |
Copyright terms: Public domain | W3C validator |