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  7878  sornom  10379  fpwwe2lem12  10751  nn0le2is012  12787  hashv01gt1  14513  hash1to3  14661  cshwshashlem1  17299  zabsle1  27650  nogesgn1o  28057  ltssolem1  28059  nosep1o  28065  colinearalg  29515  frgrregorufr0  30952  frege129d  44953