![]() |
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 1415 | . 2 ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒)) | |
2 | 3orrot 1077 | . 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑)) | |
3 | 1, 2 | sylib 208 | 1 ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ w3o 1071 |
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 197 df-or 384 df-3or 1073 |
This theorem is referenced by: 3mix3i 1420 3mix3d 1423 3jaob 1539 tppreqb 4481 tpres 6630 onzsl 7211 sornom 9291 fpwwe2lem13 9656 nn0le2is012 11633 nn01to3 11974 qbtwnxr 12224 hash1to3 13465 cshwshashlem1 16004 ostth 25527 nolesgn2o 32130 sltsolem1 32132 btwncolinear1 32482 tpid3gVD 39576 limcicciooub 40372 dfxlim2v 40576 pfxnd 41905 |
Copyright terms: Public domain | W3C validator |