Theorem 3mix1 1330

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

Syntax hints:   → wi 4   ∨ wo 846   ∨ w3o 1086

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 207  df-or 847  df-3or 1088

This theorem is referenced by:  3mix2  1331  3mix3  1332  3mix1i  1333  3mix1d  1336  3jaobOLD  1427  tppreqb  4830  onzsl  7883  sornom  10346  fpwwe2lem12  10711  nn0le2is012  12707  hashv01gt1  14394  hash1to3  14541  cshwshashlem1  17143  zabsle1  27358  nogesgn1o  27736  sltsolem1  27738  nosep1o  27744  colinearalg  28943  frgrregorufr0  30356  frege129d  43725