![]() |
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 1327 | . 2 ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒)) | |
2 | 3orrot 1089 | . 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑)) | |
3 | 1, 2 | sylib 217 | 1 ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ w3o 1083 |
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 846 df-3or 1085 |
This theorem is referenced by: 3mix3i 1332 3mix3d 1335 3jaobOLD 1424 tppreqb 4814 tpres 7220 onzsl 7858 sornom 10322 fpwwe2lem12 10687 nn0le2is012 12680 nn01to3 12979 qbtwnxr 13235 hash1to3 14512 swrdnd0 14667 pfxnd 14697 cshwshashlem1 17100 ostth 27671 nolesgn2o 27704 sltsolem1 27708 nosep2o 27715 btwncolinear1 35895 tpid3gVD 44536 limcicciooub 45276 dfxlim2v 45486 |
Copyright terms: Public domain | W3C validator |