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 864 | . 2 ⊢ (𝜑 → (𝜑 ∨ (𝜓 ∨ 𝜒))) | |
2 | 3orass 1089 | . 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) | |
3 | 1, 2 | sylibr 233 | 1 ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 844 ∨ w3o 1085 |
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 845 df-3or 1087 |
This theorem is referenced by: 3mix2 1330 3mix3 1331 3mix1i 1332 3mix1d 1335 3jaob 1425 tppreqb 4738 onzsl 7693 sornom 10033 fpwwe2lem12 10398 nn0le2is012 12384 hashv01gt1 14059 hash1to3 14205 cshwshashlem1 16797 zabsle1 26444 colinearalg 27278 frgrregorufr0 28688 nogesgn1o 33876 sltsolem1 33878 nosep1o 33884 frege129d 41371 |
Copyright terms: Public domain | W3C validator |