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 1326 | . 2 ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒)) | |
2 | 3orrot 1088 | . 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑)) | |
3 | 1, 2 | sylib 220 | 1 ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ w3o 1082 |
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 209 df-or 844 df-3or 1084 |
This theorem is referenced by: 3mix3i 1331 3mix3d 1334 3jaob 1422 tppreqb 4740 tpres 6965 onzsl 7563 sornom 9701 fpwwe2lem13 10066 nn0le2is012 12049 nn01to3 12344 qbtwnxr 12596 hash1to3 13852 swrdnd0 14021 pfxnd 14051 cshwshashlem1 16431 ostth 26217 nolesgn2o 33180 sltsolem1 33182 btwncolinear1 33532 tpid3gVD 41183 limcicciooub 41925 dfxlim2v 42135 |
Copyright terms: Public domain | W3C validator |