![]() |
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 866 | . 2 ⊢ (𝜑 → (𝜑 ∨ (𝜓 ∨ 𝜒))) | |
2 | 3orass 1091 | . 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) | |
3 | 1, 2 | sylibr 233 | 1 ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 846 ∨ w3o 1087 |
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 847 df-3or 1089 |
This theorem is referenced by: 3mix2 1332 3mix3 1333 3mix1i 1334 3mix1d 1337 3jaob 1427 tppreqb 4806 onzsl 7829 sornom 10267 fpwwe2lem12 10632 nn0le2is012 12621 hashv01gt1 14300 hash1to3 14447 cshwshashlem1 17024 zabsle1 26778 nogesgn1o 27155 sltsolem1 27157 nosep1o 27163 colinearalg 28147 frgrregorufr0 29556 frege129d 42446 |
Copyright terms: Public domain | W3C validator |