| 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 1331 | . 2 ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒)) | |
| 2 | 3orrot 1092 | . 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑)) | |
| 3 | 1, 2 | sylib 218 | 1 ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∨ w3o 1086 |
| 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 849 df-3or 1088 |
| This theorem is referenced by: 3mix3i 1336 3mix3d 1339 3jaobOLD 1429 tppreqb 4805 tpres 7221 onzsl 7867 sornom 10317 fpwwe2lem12 10682 nn0le2is012 12682 nn01to3 12983 qbtwnxr 13242 hash1to3 14531 swrdnd0 14695 pfxnd 14725 cshwshashlem1 17133 ostth 27683 nolesgn2o 27716 sltsolem1 27720 nosep2o 27727 btwncolinear1 36070 tpid3gVD 44862 limcicciooub 45652 dfxlim2v 45862 |
| Copyright terms: Public domain | W3C validator |