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

Syntax hints:   → wi 4   ∨ wo 860   ∨ w3o 1102

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 210  df-or 861  df-3or 1104

This theorem is referenced by:  3mix2  1350  3mix3  1351  3mix1i  1352  3mix1d  1355  tppreqb  4773  onzsl  7838  sornom  10256  fpwwe2lem12  10622  nn0le2is012  12655  hashv01gt1  14377  hash1to3  14525  cshwshashlem1  17150  zabsle1  27460  nogesgn1o  27837  ltssolem1  27839  nosep1o  27845  colinearalg  29260  frgrregorufr0  30675  frege129d  44509