Theorem 3mix1 1331

Description: Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)

Assertion

Ref	Expression
3mix1	⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒))

Proof of Theorem 3mix1

Step	Hyp	Ref	Expression
1		orc 867	. 2 ⊢ (𝜑 → (𝜑 ∨ (𝜓 ∨ 𝜒)))
2		3orass 1089	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3	1, 2	sylibr 234	1 ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒))

Syntax hints:   → wi 4   ∨ wo 847   ∨ 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 207  df-or 848  df-3or 1087

This theorem is referenced by:  3mix2  1332  3mix3  1333  3mix1i  1334  3mix1d  1337  3jaobOLD  1429  tppreqb  4769  onzsl  7822  sornom  10230  fpwwe2lem12  10595  nn0le2is012  12598  hashv01gt1  14310  hash1to3  14457  cshwshashlem1  17066  zabsle1  27207  nogesgn1o  27585  sltsolem1  27587  nosep1o  27593  colinearalg  28837  frgrregorufr0  30253  frege129d  43752