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 237 | 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 210 df-or 847 df-3or 1089 |
This theorem is referenced by: 3mix2 1332 3mix3 1333 3mix1i 1334 3mix1d 1337 3jaob 1427 tppreqb 4693 onzsl 7580 sornom 9777 fpwwe2lem12 10142 nn0le2is012 12127 hashv01gt1 13797 hash1to3 13943 cshwshashlem1 16532 zabsle1 26032 colinearalg 26856 frgrregorufr0 28261 nogesgn1o 33517 sltsolem1 33519 nosep1o 33525 frege129d 40917 |
Copyright terms: Public domain | W3C validator |