![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3mix3 | Structured version Visualization version GIF version |
Description: Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.) |
Ref | Expression |
---|---|
3mix3 | ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3mix1 1430 | . 2 ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒)) | |
2 | 3orrot 1113 | . 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑)) | |
3 | 1, 2 | sylib 210 | 1 ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ w3o 1107 |
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 199 df-or 875 df-3or 1109 |
This theorem is referenced by: 3mix3i 1435 3mix3d 1438 3jaob 1552 tppreqb 4524 tpres 6695 onzsl 7280 sornom 9387 fpwwe2lem13 9752 nn0le2is012 11731 nn01to3 12026 qbtwnxr 12280 hash1to3 13522 swrdnd0 13686 pfxnd 13730 cshwshashlem1 16130 ostth 25680 nolesgn2o 32337 sltsolem1 32339 btwncolinear1 32689 tpid3gVD 39838 limcicciooub 40613 dfxlim2v 40817 |
Copyright terms: Public domain | W3C validator |