| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 3mix1 | Structured version Visualization version GIF version | ||
| Description: Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.) |
| Ref | Expression |
|---|---|
| 3mix1 | ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | orc 868 | . 2 ⊢ (𝜑 → (𝜑 ∨ (𝜓 ∨ 𝜒))) | |
| 2 | 3orass 1090 | . 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) | |
| 3 | 1, 2 | sylibr 234 | 1 ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∨ wo 848 ∨ 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: 3mix2 1332 3mix3 1333 3mix1i 1334 3mix1d 1337 3jaobOLD 1429 tppreqb 4805 onzsl 7867 sornom 10317 fpwwe2lem12 10682 nn0le2is012 12682 hashv01gt1 14384 hash1to3 14531 cshwshashlem1 17133 zabsle1 27340 nogesgn1o 27718 sltsolem1 27720 nosep1o 27726 colinearalg 28925 frgrregorufr0 30343 frege129d 43776 |
| Copyright terms: Public domain | W3C validator |