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  7843  sornom  10282  fpwwe2lem12  10654  nn0le2is012  12688  hashv01gt1  14412  hash1to3  14560  cshwshashlem1  17190  zabsle1  27535  nogesgn1o  27912  ltssolem1  27914  nosep1o  27920  colinearalg  29370  frgrregorufr0  30807  frege129d  44606