Theorem 3mix1 1329

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

Syntax hints:   → wi 4   ∨ wo 844   ∨ 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 206  df-or 845  df-3or 1087

This theorem is referenced by:  3mix2  1330  3mix3  1331  3mix1i  1332  3mix1d  1335  3jaob  1425  tppreqb  4738  onzsl  7693  sornom  10033  fpwwe2lem12  10398  nn0le2is012  12384  hashv01gt1  14059  hash1to3  14205  cshwshashlem1  16797  zabsle1  26444  colinearalg  27278  frgrregorufr0  28688  nogesgn1o  33876  sltsolem1  33878  nosep1o  33884  frege129d  41371