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 863 | . 2 ⊢ (𝜑 → (𝜑 ∨ (𝜓 ∨ 𝜒))) | |
2 | 3orass 1086 | . 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) | |
3 | 1, 2 | sylibr 236 | 1 ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 843 ∨ w3o 1082 |
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 209 df-or 844 df-3or 1084 |
This theorem is referenced by: 3mix2 1327 3mix3 1328 3mix1i 1329 3mix1d 1332 3jaob 1422 tppreqb 4740 onzsl 7563 sornom 9701 fpwwe2lem13 10066 nn0le2is012 12049 hashv01gt1 13708 hash1to3 13852 cshwshashlem1 16431 zabsle1 25874 colinearalg 26698 frgrregorufr0 28105 sltsolem1 33182 nosep1o 33188 frege129d 40115 |
Copyright terms: Public domain | W3C validator |