Theorem 3mix1 1230

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

Syntax hints:   → wi 4   ∨ wo 383   ∨ w3o 1036

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 197  df-or 385  df-3or 1038

This theorem is referenced by:  3mix2  1231  3mix3  1232  3mix1i  1233  3mix1d  1236  3jaob  1390  tppreqb  4336  onzsl  7046  sornom  9099  fpwwe2lem13  9464  nn0le2is012  11441  hashv01gt1  13133  hash1to3  13273  cshwshashlem1  15802  zabsle1  25021  colinearalg  25790  frgrregorufr0  27188  sltsolem1  31826  nosep1o  31832  frege129d  38055