Theorem 3mix1 1349

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 881	. 2 ⊢ (𝜑 → (𝜑 ∨ (𝜓 ∨ 𝜒)))
2		3orass 1106	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3	1, 2	sylibr 237	1 ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒))

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   ∨ w3o 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862  df-3or 1104

This theorem is used by:  3mix2  1350  3mix3  1351  3mix1i  1352  3mix1d  1355  tppreqb  4768  onzsl  7857  sornom  10355  fpwwe2lem12  10727  nn0le2is012  12763  hashv01gt1  14489  hash1to3  14637  cshwshashlem1  17273  zabsle1  27623  nogesgn1o  28030  ltssolem1  28032  nosep1o  28038  colinearalg  29488  frgrregorufr0  30925  frege129d  44762